Intuitionize 19.30 in iset.mm
Intuitionize 19.30 in iset.mm

Replace 19.30 with 19.30dc and move it back to where 19.30 is
in set.mm (between 19.25 and 19.43). Write a proof for it
which follows fairly readily from the decidability condition.

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