let X be set ; :: thesis: for A, B, C being Subset-Family of X holds INTERSECTION (A,(UNION (B,C))) c= UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
let A, B, C be Subset-Family of X; :: thesis: INTERSECTION (A,(UNION (B,C))) c= UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in INTERSECTION (A,(UNION (B,C))) or x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) )
assume x in INTERSECTION (A,(UNION (B,C))) ; :: thesis: x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
then consider X, Y being set such that
Q1: ( X in A & Y in UNION (B,C) & x = X /\ Y ) by SETFAM_1:def 5;
consider Z, W being set such that
Q2: ( Z in B & W in C & Y = Z \/ W ) by Q1, SETFAM_1:def 4;
Q3: x = (X /\ Z) \/ (X /\ W) by Q1, Q2, XBOOLE_1:23;
Q4: X /\ Z in INTERSECTION (A,B) by Q1, Q2, SETFAM_1:def 5;
X /\ W in INTERSECTION (A,C) by Q1, Q2, SETFAM_1:def 5;
hence x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) by Q3, Q4, SETFAM_1:def 4; :: thesis: verum