Intuitionize opnz in iset.mm
Intuitionize opnz in iset.mm

Change non-empty to inhabited, rename to opm , and prove it a
different way.

opm would also imply the reverse direction of opnz but I guess
I'll add that later if there seems to be a need for it.

metamath/set.mm,metamath/set.mm,metamath/set.mm