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)))

A1: UNION (A,(INTERSECTION (B,C))) c= INTERSECTION ((UNION (A,B)),(UNION (A,C))) by Lm1;

INTERSECTION ((UNION (A,B)),(UNION (A,C))) c= UNION (A,(INTERSECTION (B,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)))

A1: UNION (A,(INTERSECTION (B,C))) c= INTERSECTION ((UNION (A,B)),(UNION (A,C))) by Lm1;

INTERSECTION ((UNION (A,B)),(UNION (A,C))) c= UNION (A,(INTERSECTION (B,C)))

proof

hence
UNION (A,(INTERSECTION (B,C))) = INTERSECTION ((UNION (A,B)),(UNION (A,C)))
by A1; :: thesis: verum
let x be object ; :: 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

A2: ( 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

A3: ( X1 in A & X2 in B & X = X1 \/ X2 ) by A2, SETFAM_1:def 4;

consider Y1, Y2 being set such that

A4: ( Y1 in A & Y2 in C & Y = Y1 \/ Y2 ) by A2, SETFAM_1:def 4;

A5: x = (X1 /\ (Y1 \/ Y2)) \/ (X2 /\ (Y1 \/ Y2)) by A2, A3, A4, XBOOLE_1:23

.= ((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 A3, A4, Th28;

then A6: ( (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 A4, Th28, XBOOLE_1:17;

then X2 /\ Y1 c= max A ;

then A7: ( min A c= (X1 /\ Y1) \/ (X2 /\ Y1) & (X1 /\ Y1) \/ (X2 /\ Y1) c= max A ) by A6, XBOOLE_1:8, XBOOLE_1:10;

( X1 c= max A & X1 /\ Y2 c= X1 ) by A3, Th28, XBOOLE_1:17;

then X1 /\ Y2 c= max A ;

then ((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2) c= max A by A7, XBOOLE_1:8;

then ( min A c= ((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2) & ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) c= max A ) by A7, XBOOLE_1:4, 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 A8: ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) in A by Th28;

X2 /\ Y2 in INTERSECTION (B,C) by A3, A4, SETFAM_1:def 5;

hence x in UNION (A,(INTERSECTION (B,C))) by A8, A5, SETFAM_1:def 4; :: thesis: verum

end;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

A2: ( 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

A3: ( X1 in A & X2 in B & X = X1 \/ X2 ) by A2, SETFAM_1:def 4;

consider Y1, Y2 being set such that

A4: ( Y1 in A & Y2 in C & Y = Y1 \/ Y2 ) by A2, SETFAM_1:def 4;

A5: x = (X1 /\ (Y1 \/ Y2)) \/ (X2 /\ (Y1 \/ Y2)) by A2, A3, A4, XBOOLE_1:23

.= ((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 A3, A4, Th28;

then A6: ( (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 A4, Th28, XBOOLE_1:17;

then X2 /\ Y1 c= max A ;

then A7: ( min A c= (X1 /\ Y1) \/ (X2 /\ Y1) & (X1 /\ Y1) \/ (X2 /\ Y1) c= max A ) by A6, XBOOLE_1:8, XBOOLE_1:10;

( X1 c= max A & X1 /\ Y2 c= X1 ) by A3, Th28, XBOOLE_1:17;

then X1 /\ Y2 c= max A ;

then ((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2) c= max A by A7, XBOOLE_1:8;

then ( min A c= ((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2) & ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) c= max A ) by A7, XBOOLE_1:4, 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 A8: ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) in A by Th28;

X2 /\ Y2 in INTERSECTION (B,C) by A3, A4, SETFAM_1:def 5;

hence x in UNION (A,(INTERSECTION (B,C))) by A8, A5, SETFAM_1:def 4; :: thesis: verum