theorem Th9: :: ZFREFLE1:9

for M1, M2 being non empty set st M1 is_elementary_subsystem_of M2 holds
M1 <==> M2