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

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