Add enqbreq2 to iset.mm
Add enqbreq2 to iset.mm

The statement of the theorem is as in set.mm. The proof only
requires one minor change, from mulcompi to mulcompig (the
conditions of the latter are already met, so easy to hook in).

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