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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in INTERSECTION (UNION A,B),(UNION A,C) or x in UNION A,(INTERSECTION B,C) )
assume x in INTERSECTION (UNION A,B),(UNION A,C) ; :: thesis: x in UNION A,(INTERSECTION B,C)
then consider X, Y being set such that
a0: ( X in UNION A,B & Y in UNION A,C & x = X /\ Y ) by SETFAM_1:def 5;
consider X1, X2 being set such that
a1: ( X1 in A & X2 in B & X = X1 \/ X2 ) by a0, SETFAM_1:def 4;
consider Y1, Y2 being set such that
a2: ( Y1 in A & Y2 in C & Y = Y1 \/ Y2 ) by a0, SETFAM_1:def 4;
a3: x = (X1 /\ (Y1 \/ Y2)) \/ (X2 /\ (Y1 \/ Y2)) by XBOOLE_1:23, a0, a1, a2
.= ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ (Y1 \/ Y2)) by XBOOLE_1:23
.= ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ ((X2 /\ Y1) \/ (X2 /\ Y2)) by XBOOLE_1:23
.= (((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1)) \/ (X2 /\ Y2) by XBOOLE_1:4 ;
set A1 = min A;
set A2 = max A;
( min A c= X1 & X1 c= max A & min A c= Y1 & Y1 c= max A ) by a1, a2, Nowe1;
then m2: ( (min A) /\ (min A) c= X1 /\ Y1 & X1 /\ Y1 c= (max A) /\ (max A) ) by XBOOLE_1:27;
( Y1 c= max A & X2 /\ Y1 c= Y1 ) by a2, Nowe1, XBOOLE_1:17;
then X2 /\ Y1 c= max A by XBOOLE_1:1;
then m3: ( min A c= (X1 /\ Y1) \/ (X2 /\ Y1) & (X1 /\ Y1) \/ (X2 /\ Y1) c= max A ) by XBOOLE_1:10, XBOOLE_1:8, m2;
( X1 c= max A & X1 /\ Y2 c= X1 ) by a1, Nowe1, XBOOLE_1:17;
then X1 /\ Y2 c= max A by XBOOLE_1:1;
then ((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2) c= max A by m3, XBOOLE_1:8;
then ( min A c= ((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2) & ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) c= max A ) by XBOOLE_1:4, m3, XBOOLE_1:10;
then ( min A c= ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) & ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) c= max A ) by XBOOLE_1:4;
then l1: ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) in A by Nowe1;
X2 /\ Y2 in INTERSECTION B,C by a1, a2, SETFAM_1:def 5;
hence x in UNION A,(INTERSECTION B,C) by l1, a3, SETFAM_1:def 4; :: thesis: verum

end;

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