let U be non empty set ; :: thesis: for A1, A2, B1, B2 being Subset of U st A1 c= A2 & B1 c= B2 holds
INTERSECTION ((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 INTERSECTION ((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: INTERSECTION ((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 = INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2)));
thus INTERSECTION ((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= INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in INTERSECTION ((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 INTERSECTION ((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 5;
xx c= X by A3, XBOOLE_1:17;
then A4: x is Subset of U by A3, XBOOLE_1:1;
A5: A1 c= X by Th1, A3;
B1 c= Y by Th1, A3;
then A6: A1 /\ B1 c= xx by A5, A3, XBOOLE_1:27;
A7: X c= A2 by Th1, A3;
Y c= B2 by Th1, A3;
then xx c= A2 /\ B2 by A7, A3, XBOOLE_1:27;
hence x in { C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 ) } by A6, A4; :: thesis: verum
end;
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 INTERSECTION ((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 INTERSECTION ((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: ((xx \/ A1) /\ A2) /\ ((xx \/ B1) /\ B2) = (xx \/ A1) /\ (A2 /\ ((xx \/ B1) /\ B2)) by XBOOLE_1:16
.= (xx \/ A1) /\ ((xx \/ B1) /\ (B2 /\ A2)) by XBOOLE_1:16
.= ((xx \/ A1) /\ (xx \/ B1)) /\ (A2 /\ B2) by XBOOLE_1:16
.= x by A9, A10, XBOOLE_1:24 ;
A1 /\ A2 = A1 by A1, XBOOLE_1:28;
then (xx \/ A1) /\ A2 = (xx /\ A2) \/ A1 by XBOOLE_1:23;
then A12: A1 c= (xx \/ A1) /\ A2 by XBOOLE_1:7;
(xx \/ A1) /\ A2 c= A2 by XBOOLE_1:17;
then A13: (xx \/ A1) /\ A2 in Inter (A1,A2) by A12;
B1 /\ B2 = B1 by A2, XBOOLE_1:28;
then (xx \/ B1) /\ B2 = (xx /\ B2) \/ B1 by XBOOLE_1:23;
then A14: 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 A14;
hence x in INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) by A11, A13, SETFAM_1:def 5; :: thesis: verum