Add empty set existence section to iset.mm
Add empty set existence section to iset.mm

This is the section "Theorems requiring empty set existence",
copied verbatim from set.mm. Follow up changes will be needed
for it to verify.

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