thus
( A = B implies ( A ``1 = B ``1 & A ``2 = B ``2 ) )
; ( A ``1 = B ``1 & A ``2 = B ``2 implies A = B )
assume that
A1:
A ``1 = B ``1
and
A2:
A ``2 = B ``2
; A = B
A3:
A c= B
proof
let x be
object ;
TARSKI:def 3 ( not x in A or x in B )
assume A4:
x in A
;
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;
verum
end;
B c= A
proof
let x be
object ;
TARSKI:def 3 ( not x in B or x in A )
assume A12:
x in B
;
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;
verum
end;
hence
A = B
by A3; verum