let E be non empty set ; :: thesis: ( E is epsilon-transitive implies E |= the_axiom_of_extensionality )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def 2 :: thesis: E |= the_axiom_of_extensionality
E |= (All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1))

proof

let f be Function of VAR,E; :: according to ZF_MODEL:def 5 :: thesis: E,f |= (All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1))

now :: thesis: ( E,f |= All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) implies E,f |= (x. 0) '=' (x. 1) )

assume A2: E,f |= All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) ; :: thesis: E,f |= (x. 0) '=' (x. 1)
f . (x. 0) = f . (x. 1)

proof

thus for a being object st a in f . (x. 0) holds
a in f . (x. 1) :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: f . (x. 1) c= f . (x. 0)

proof

let a be object ; :: thesis: ( a in f . (x. 0) implies a in f . (x. 1) )
assume A3: a in f . (x. 0) ; :: thesis: a in f . (x. 1)
f . (x. 0) c= E by A1;
then reconsider a9 = a as Element of E by A3;
set g = f +* ((x. 2),a9);
A4: (f +* ((x. 2),a9)) . (x. 1) = f . (x. 1) by FUNCT_7:32;
for x being Variable st (f +* ((x. 2),a9)) . x <> f . x holds
x. 2 = x by FUNCT_7:32;
then E,f +* ((x. 2),a9) |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A2, ZF_MODEL:16;
then A5: ( E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 0) iff E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:19;
( (f +* ((x. 2),a9)) . (x. 2) = a9 & (f +* ((x. 2),a9)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;
hence a in f . (x. 1) by A3, A5, A4, ZF_MODEL:13; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f . (x. 1) or a in f . (x. 0) )
assume A6: a in f . (x. 1) ; :: thesis: a in f . (x. 0)
f . (x. 1) c= E by A1;
then reconsider a9 = a as Element of E by A6;
set g = f +* ((x. 2),a9);
A7: (f +* ((x. 2),a9)) . (x. 1) = f . (x. 1) by FUNCT_7:32;
for x being Variable st (f +* ((x. 2),a9)) . x <> f . x holds
x. 2 = x by FUNCT_7:32;
then E,f +* ((x. 2),a9) |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A2, ZF_MODEL:16;
then A8: ( E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 0) iff E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:19;
( (f +* ((x. 2),a9)) . (x. 2) = a9 & (f +* ((x. 2),a9)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;
hence a in f . (x. 0) by A6, A8, A7, ZF_MODEL:13; :: thesis: verum

end;

hence E,f |= (x. 0) '=' (x. 1) by ZF_MODEL:12; :: thesis: verum

end;

hence E,f |= (All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)) by ZF_MODEL:18; :: thesis: verum

end;

then E |= All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) by ZF_MODEL:23;
hence E |= the_axiom_of_extensionality by ZF_MODEL:23; :: thesis: verum