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

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 set 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 set ; :: 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:34;
for x being Variable st (f +* (x. 2),a9) . x <> f . x holds
x. 2 = x by FUNCT_7:34;
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:34, FUNCT_7:130;
hence a in f . (x. 1) by A3, A5, A4, ZF_MODEL:13; :: thesis: verum

end;

let a be set ; :: 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:34;
for x being Variable st (f +* (x. 2),a9) . x <> f . x holds
x. 2 = x by FUNCT_7:34;
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:34, FUNCT_7:130;
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:25;
hence E |= the_axiom_of_extensionality by ZF_MODEL:25; :: thesis: verum