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
d1:
A c= B
proof
let x be
set ;
TARSKI:def 3 ( not x in A or x in B )
assume T0:
x in A
;
x in B
consider A1,
B1 being
Subset of
U such that T1:
A = Inter (
A1,
B1)
by WW;
consider C1 being
Subset of
U such that W1:
A = Inter (
(A ``1),
C1)
by Def4;
v1:
A1 = B ``1
by A1, T1, Pik, W1;
consider C2 being
Subset of
U such that V1:
B = Inter (
(B ``1),
C2)
by Def4;
consider D1 being
Subset of
U such that V2:
A = Inter (
D1,
(A ``2))
by Def5;
v4:
B ``2 = B1
by A2, V2, T1, Pik;
consider D2 being
Subset of
U such that V3:
B = Inter (
D2,
(B ``2))
by Def5;
thus
x in B
by T0, T1, v1, V1, v4, V3, Pik;
verum
end;
B c= A
proof
let x be
set ;
TARSKI:def 3 ( not x in B or x in A )
assume T0:
x in B
;
x in A
consider A1,
B1 being
Subset of
U such that T1:
B = Inter (
A1,
B1)
by WW;
consider C1 being
Subset of
U such that W1:
B = Inter (
(B ``1),
C1)
by Def4;
v1:
A ``1 = A1
by A1, W1, Pik, T1;
consider C2 being
Subset of
U such that V1:
A = Inter (
(A ``1),
C2)
by Def4;
consider D1 being
Subset of
U such that V2:
B = Inter (
D1,
(B ``2))
by Def5;
v4:
A ``2 = B1
by A2, V2, T1, Pik;
consider D2 being
Subset of
U such that V3:
A = Inter (
D2,
(A ``2))
by Def5;
thus
x in A
by T0, T1, v1, V1, v4, V3, Pik;
verum
end;
hence
A = B
by d1, XBOOLE_0:def 10; verum