let M1, M2 be non empty set ; :: thesis: ( M1 is_elementary_subsystem_of M2 implies M1 <==> M2 )
assume that
M1 c= M2 and
A1: for H being ZF-formula
for v being Function of VAR ,M1 holds
( M1,v |= H iff M2,M2 ! v |= H ) ; :: according to ZFREFLE1:def 3 :: thesis: M1 <==> M2
let H be ZF-formula; :: according to ZFREFLE1:def 2 :: thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) )
assume A2: Free H = {} ; :: thesis: ( M1 |= H iff M2 |= H )
thus ( M1 |= H implies M2 |= H ) :: thesis: ( M2 |= H implies M1 |= H )

proof

assume A3: for v1 being Function of VAR ,M1 holds M1,v1 |= H ; :: according to ZF_MODEL:def 5 :: thesis: M2 |= H
consider v1 being Function of VAR ,M1;
M1,v1 |= H by A3;
then A4: M2,M2 ! v1 |= H by A1;
let v2 be Function of VAR ,M2; :: according to ZF_MODEL:def 5 :: thesis: M2,v2 |= H
for x being Variable st x in Free H holds
v2 . x = (M2 ! v1) . x by A2;
hence M2,v2 |= H by A4, ZF_LANG1:84; :: thesis: verum

end;

assume A5: for v2 being Function of VAR ,M2 holds M2,v2 |= H ; :: according to ZF_MODEL:def 5 :: thesis: M1 |= H
let v1 be Function of VAR ,M1; :: according to ZF_MODEL:def 5 :: thesis: M1,v1 |= H
M2,M2 ! v1 |= H by A5;
hence M1,v1 |= H by A1; :: thesis: verum