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