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 set ; :: 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