thus
( A = B implies ( A ``1 = B ``1 & A ``2 = B ``2 ) )
; :: thesis: ( A ``1 = B ``1 & A ``2 = B ``2 implies A = B )

assume that

A1: A ``1 = B ``1 and

A2: A ``2 = B ``2 ; :: thesis: A = B

A3: A c= B

assume that

A1: A ``1 = B ``1 and

A2: A ``2 = B ``2 ; :: thesis: A = B

A3: A c= B

proof

B c= A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )

assume A4: x in A ; :: thesis: x in B

consider A1, B1 being Subset of U such that

A5: A = Inter (A1,B1) by Def2;

consider C1 being Subset of U such that

A6: A = Inter ((A ``1),C1) by Def5;

A7: A1 = B ``1 by A1, A5, Th6, A6;

consider C2 being Subset of U such that

A8: B = Inter ((B ``1),C2) by Def5;

consider D1 being Subset of U such that

A9: A = Inter (D1,(A ``2)) by Def6;

A10: B ``2 = B1 by A2, A9, A5, Th6;

consider D2 being Subset of U such that

A11: B = Inter (D2,(B ``2)) by Def6;

thus x in B by A4, A5, A7, A8, A10, A11, Th6; :: thesis: verum

end;assume A4: x in A ; :: thesis: x in B

consider A1, B1 being Subset of U such that

A5: A = Inter (A1,B1) by Def2;

consider C1 being Subset of U such that

A6: A = Inter ((A ``1),C1) by Def5;

A7: A1 = B ``1 by A1, A5, Th6, A6;

consider C2 being Subset of U such that

A8: B = Inter ((B ``1),C2) by Def5;

consider D1 being Subset of U such that

A9: A = Inter (D1,(A ``2)) by Def6;

A10: B ``2 = B1 by A2, A9, A5, Th6;

consider D2 being Subset of U such that

A11: B = Inter (D2,(B ``2)) by Def6;

thus x in B by A4, A5, A7, A8, A10, A11, Th6; :: thesis: verum

proof

hence
A = B
by A3; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in A )

assume A12: x in B ; :: thesis: x in A

consider A1, B1 being Subset of U such that

A13: B = Inter (A1,B1) by Def2;

consider C1 being Subset of U such that

A14: B = Inter ((B ``1),C1) by Def5;

A15: A ``1 = A1 by A1, A14, Th6, A13;

consider C2 being Subset of U such that

A16: A = Inter ((A ``1),C2) by Def5;

consider D1 being Subset of U such that

A17: B = Inter (D1,(B ``2)) by Def6;

A18: A ``2 = B1 by A2, A17, A13, Th6;

consider D2 being Subset of U such that

A19: A = Inter (D2,(A ``2)) by Def6;

thus x in A by A12, A13, A15, A16, A18, A19, Th6; :: thesis: verum

end;assume A12: x in B ; :: thesis: x in A

consider A1, B1 being Subset of U such that

A13: B = Inter (A1,B1) by Def2;

consider C1 being Subset of U such that

A14: B = Inter ((B ``1),C1) by Def5;

A15: A ``1 = A1 by A1, A14, Th6, A13;

consider C2 being Subset of U such that

A16: A = Inter ((A ``1),C2) by Def5;

consider D1 being Subset of U such that

A17: B = Inter (D1,(B ``2)) by Def6;

A18: A ``2 = B1 by A2, A17, A13, Th6;

consider D2 being Subset of U such that

A19: A = Inter (D2,(A ``2)) by Def6;

thus x in A by A12, A13, A15, A16, A18, A19, Th6; :: thesis: verum