let T1, T2 be set ; :: thesis: ( ( for x being set holds
( x in T1 iff ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) ) ) & ( for x being set holds
( x in T2 iff ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) ) ) implies T1 = T2 )
assume A5: ( ( for x being set holds
( x in T1 iff ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) ) ) & ( for x being set holds
( x in T2 iff ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) ) ) & not T1 = T2 ) ; :: thesis: contradiction
then consider x being object such that
A6: ( ( x in T1 & not x in T2 ) or ( x in T2 & not x in T1 ) ) by TARSKI:2;
( x in T2 iff for a, y being set holds
( not x = [a,y] or not a in dom f or not y in f . a or ex b being set st
( b in dom f & b c= a & y in f . b & not a = b ) ) ) by A5, A6;
hence contradiction by A5; :: thesis: verum