let X be set ; 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; INTERSECTION (A,(UNION (B,C))) c= UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
let x be object ; TARSKI:def 3 ( 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)))
; 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; verum