let X be set ; :: thesis: for A, B, C being non empty ordered Subset-Family of X holds INTERSECTION A,(UNION B,C) = UNION (INTERSECTION A,B),(INTERSECTION A,C)
let A, B, C be non empty ordered Subset-Family of X; :: thesis: INTERSECTION A,(UNION B,C) = UNION (INTERSECTION A,B),(INTERSECTION A,C)
R: INTERSECTION A,(UNION B,C) c= UNION (INTERSECTION A,B),(INTERSECTION A,C) by Lemacik2;
UNION (INTERSECTION A,B),(INTERSECTION A,C) c= INTERSECTION A,(UNION B,C)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UNION (INTERSECTION A,B),(INTERSECTION A,C) or x in INTERSECTION A,(UNION B,C) )
assume x in UNION (INTERSECTION A,B),(INTERSECTION A,C) ; :: thesis: x in INTERSECTION A,(UNION B,C)
then consider X, Y being set such that
Q5: ( X in INTERSECTION A,B & Y in INTERSECTION A,C & x = X \/ Y ) by SETFAM_1:def 4;
consider X1, X2 being set such that
Q6: ( X1 in A & X2 in B & X = X1 /\ X2 ) by SETFAM_1:def 5, Q5;
consider Y1, Y2 being set such that
Q7: ( Y1 in A & Y2 in C & Y = Y1 /\ Y2 ) by SETFAM_1:def 5, Q5;
Q8: x = ((X1 /\ X2) \/ Y1) /\ ((X1 /\ X2) \/ Y2) by XBOOLE_1:24, Q5, Q6, Q7
.= (Y1 \/ (X1 /\ X2)) /\ ((Y2 \/ X1) /\ (Y2 \/ X2)) by XBOOLE_1:24
.= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ ((Y2 \/ X1) /\ (Y2 \/ X2)) by XBOOLE_1:24
.= (((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1)) /\ (Y2 \/ X2) by XBOOLE_1:16 ;
set A1 = min A;
set A2 = max A;
ww: ( min A c= Y1 & min A c= X1 ) by Q6, Q7, Nowe1;
then w0: (min A) \/ (min A) c= Y1 \/ X1 by XBOOLE_1:13;
Y1 c= Y1 \/ X2 by XBOOLE_1:7;
then min A c= Y1 \/ X2 by ww, XBOOLE_1:1;
then w2: (min A) /\ (min A) c= (Y1 \/ X1) /\ (Y1 \/ X2) by XBOOLE_1:27, w0;
( min A c= X1 & X1 c= Y2 \/ X1 ) by Nowe1, Q6, XBOOLE_1:7;
then min A c= Y2 \/ X1 by XBOOLE_1:1;
then w1: min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) by XBOOLE_1:19, w2;
( Y1 c= max A & X1 c= max A ) by Q6, Q7, Nowe1;
then ( (Y1 \/ X1) /\ ((Y1 \/ X2) /\ (Y2 \/ X1)) c= Y1 \/ X1 & Y1 \/ X1 c= max A ) by XBOOLE_1:8, XBOOLE_1:17;
then ( min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) & (Y1 \/ X1) /\ ((Y1 \/ X2) /\ (Y2 \/ X1)) c= max A ) by XBOOLE_1:1, w1;
then ( min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) & ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) c= max A ) by XBOOLE_1:16;
then Q9: ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) in A by Nowe1;
Y2 \/ X2 in UNION B,C by SETFAM_1:def 4, Q6, Q7;
hence x in INTERSECTION A,(UNION B,C) by SETFAM_1:def 5, Q8, Q9; :: thesis: verum

end;

hence INTERSECTION A,(UNION B,C) = UNION (INTERSECTION A,B),(INTERSECTION A,C) by R, XBOOLE_0:def 10; :: thesis: verum