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

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