let U be non empty set ; for A1, A2, B1, B2 being Subset of U st A1 c= A2 & B1 c= B2 holds
UNION ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) }
let A1, A2, B1, B2 be Subset of U; ( A1 c= A2 & B1 c= B2 implies UNION ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) } )
assume that
A1:
A1 c= A2
and
A2:
B1 c= B2
; UNION ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) }
set A = Inter (A1,A2);
set B = Inter (B1,B2);
set LAB = A1 \/ B1;
set UAB = A2 \/ B2;
set IT = UNION ((Inter (A1,A2)),(Inter (B1,B2)));
thus
UNION ((Inter (A1,A2)),(Inter (B1,B2))) c= { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) }
XBOOLE_0:def 10 { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) } c= UNION ((Inter (A1,A2)),(Inter (B1,B2)))proof
let x be
object ;
TARSKI:def 3 ( not x in UNION ((Inter (A1,A2)),(Inter (B1,B2))) or x in { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) } )
reconsider xx =
x as
set by TARSKI:1;
assume
x in UNION (
(Inter (A1,A2)),
(Inter (B1,B2)))
;
x in { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) }
then consider X,
Y being
set such that A3:
(
X in Inter (
A1,
A2) &
Y in Inter (
B1,
B2) &
x = X \/ Y )
by SETFAM_1:def 4;
A4:
x is
Subset of
U
by A3, XBOOLE_1:8;
A5:
A1 c= X
by Th1, A3;
B1 c= Y
by Th1, A3;
then A6:
A1 \/ B1 c= xx
by A5, A3, XBOOLE_1:13;
A7:
X c= A2
by Th1, A3;
Y c= B2
by Th1, A3;
then
xx c= A2 \/ B2
by A7, A3, XBOOLE_1:13;
hence
x in { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) }
by A4, A6;
verum
end;
let x be object ; TARSKI:def 3 ( not x in { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) } or x in UNION ((Inter (A1,A2)),(Inter (B1,B2))) )
reconsider xx = x as set by TARSKI:1;
assume
x in { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) }
; x in UNION ((Inter (A1,A2)),(Inter (B1,B2)))
then consider C9 being Subset of U such that
A8:
( C9 = x & A1 \/ B1 c= C9 & C9 c= A2 \/ B2 )
;
set x1 = (xx \/ A1) /\ A2;
set x2 = (xx \/ B1) /\ B2;
A9:
(A1 \/ B1) \/ xx = x
by A8, XBOOLE_1:12;
A10:
(A2 \/ B2) /\ xx = x
by A8, XBOOLE_1:28;
A11:
A1 /\ A2 = A1
by A1, XBOOLE_1:28;
A12:
B1 /\ B2 = B1
by A2, XBOOLE_1:28;
A13: ((xx \/ A1) /\ A2) \/ ((xx \/ B1) /\ B2) =
((xx /\ A2) \/ (A1 /\ A2)) \/ ((xx \/ B1) /\ B2)
by XBOOLE_1:23
.=
((xx /\ A2) \/ A1) \/ ((xx /\ B2) \/ (B1 /\ B2))
by A11, XBOOLE_1:23
.=
(xx /\ A2) \/ (A1 \/ ((xx /\ B2) \/ B1))
by A12, XBOOLE_1:4
.=
(xx /\ A2) \/ ((xx /\ B2) \/ (A1 \/ B1))
by XBOOLE_1:4
.=
((xx /\ A2) \/ (xx /\ B2)) \/ (A1 \/ B1)
by XBOOLE_1:4
.=
x
by A9, A10, XBOOLE_1:23
;
A1 /\ A2 = A1
by A1, XBOOLE_1:28;
then
(xx \/ A1) /\ A2 = (xx /\ A2) \/ A1
by XBOOLE_1:23;
then A14:
A1 c= (xx \/ A1) /\ A2
by XBOOLE_1:7;
(xx \/ A1) /\ A2 c= A2
by XBOOLE_1:17;
then A15:
(xx \/ A1) /\ A2 in Inter (A1,A2)
by A14;
B1 /\ B2 = B1
by A2, XBOOLE_1:28;
then
(xx \/ B1) /\ B2 = (xx /\ B2) \/ B1
by XBOOLE_1:23;
then A16:
B1 c= (xx \/ B1) /\ B2
by XBOOLE_1:7;
(xx \/ B1) /\ B2 c= B2
by XBOOLE_1:17;
then
(xx \/ B1) /\ B2 in Inter (B1,B2)
by A16;
hence
x in UNION ((Inter (A1,A2)),(Inter (B1,B2)))
by A13, A15, SETFAM_1:def 4; verum