Remove oprssdm from iset.mm
Remove oprssdm from iset.mm

Looks like we'll need to revisit one way or another by the time
we get to dmaddsr (part of the construction of the reals), but
the current proof is not intuitionistic.

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