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