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 set ; :: 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 ) } )
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
B1: ( X in Inter A1,A2 & Y in Inter B1,B2 & x = X /\ Y ) by SETFAM_1:def 5;
x c= X by B1, XBOOLE_1:17;
then B2: x is Subset of U by B1, XBOOLE_1:1;
B4: A1 c= X by Lemacik, B1;
B1 c= Y by Lemacik, B1;
then B3: A1 /\ B1 c= x by B4, B1, XBOOLE_1:27;
B5: X c= A2 by Lemacik, B1;
Y c= B2 by Lemacik, B1;
then x c= A2 /\ B2 by B5, XBOOLE_1:27, B1;
hence x in { C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 ) } by B3, B2; :: thesis: verum

end;

let x be set ; :: 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) )
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
B1: ( C9 = x & A1 /\ B1 c= C9 & C9 c= A2 /\ B2 ) ;
set x1 = (x \/ A1) /\ A2;
set x2 = (x \/ B1) /\ B2;
T1: (A1 /\ B1) \/ x = x by B1, XBOOLE_1:12;
T2: (A2 /\ B2) /\ x = x by B1, XBOOLE_1:28;
T4: ((x \/ A1) /\ A2) /\ ((x \/ B1) /\ B2) = (x \/ A1) /\ (A2 /\ ((x \/ B1) /\ B2)) by XBOOLE_1:16
.= (x \/ A1) /\ ((x \/ B1) /\ (B2 /\ A2)) by XBOOLE_1:16
.= ((x \/ A1) /\ (x \/ B1)) /\ (A2 /\ B2) by XBOOLE_1:16
.= x by T1, T2, XBOOLE_1:24 ;
A1 /\ A2 = A1 by A1, XBOOLE_1:28;
then (x \/ A1) /\ A2 = (x /\ A2) \/ A1 by XBOOLE_1:23;
then H1: A1 c= (x \/ A1) /\ A2 by XBOOLE_1:7;
(x \/ A1) /\ A2 c= A2 by XBOOLE_1:17;
then Y2: (x \/ A1) /\ A2 in Inter A1,A2 by H1;
B1 /\ B2 = B1 by A2, XBOOLE_1:28;
then (x \/ B1) /\ B2 = (x /\ B2) \/ B1 by XBOOLE_1:23;
then H2: B1 c= (x \/ B1) /\ B2 by XBOOLE_1:7;
(x \/ B1) /\ B2 c= B2 by XBOOLE_1:17;
then (x \/ B1) /\ B2 in Inter B1,B2 by H2;
hence x in INTERSECTION (Inter A1,A2),(Inter B1,B2) by T4, Y2, SETFAM_1:def 5; :: thesis: verum