let U be non empty set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ) } :: according to XBOOLE_0:def 10 :: thesis: { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) } c= 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 ) } ; :: thesis: 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; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: 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 ) } :: according to XBOOLE_0:def 10 :: thesis: { 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 ; :: according to TARSKI:def 3 :: thesis: ( 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))) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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))) ; :: thesis: 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; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume x in UNION ((Inter (A1,A2)),(Inter (B1,B2))) ; :: thesis: 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; :: thesis: verum

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 ) } ; :: thesis: 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; :: thesis: verum