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
proof
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;
B c= A
proof
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;
hence A = B by A3; :: thesis: verum