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 object ; :: 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
A1: ( X in A & Y in UNION (B,C) & x = X /\ Y ) by SETFAM_1:def 5;
consider Z, W being set such that
A2: ( Z in B & W in C & Y = Z \/ W ) by A1, SETFAM_1:def 4;
A3: x = (X /\ Z) \/ (X /\ W) by A1, A2, XBOOLE_1:23;
A4: X /\ Z in INTERSECTION (A,B) by A1, A2, SETFAM_1:def 5;
X /\ W in INTERSECTION (A,C) by A1, A2, SETFAM_1:def 5;
hence x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) by A3, A4, SETFAM_1:def 4; :: thesis: verum