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

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

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

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

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

proof

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

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

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

consider Y1, Y2 being set such that

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

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

.= (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;

A6: ( min A c= Y1 & min A c= X1 ) by A3, A4, Th28;

then A7: (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 A6;

then A8: (min A) /\ (min A) c= (Y1 \/ X1) /\ (Y1 \/ X2) by A7, XBOOLE_1:27;

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

then min A c= Y2 \/ X1 ;

then A9: min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) by A8, XBOOLE_1:19;

( Y1 c= max A & X1 c= max A ) by A3, A4, Th28;

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

then ( min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) & ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) c= max A ) by XBOOLE_1:16;

then A10: ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) in A by Th28;

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

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

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

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

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

consider Y1, Y2 being set such that

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

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

.= (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;

A6: ( min A c= Y1 & min A c= X1 ) by A3, A4, Th28;

then A7: (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 A6;

then A8: (min A) /\ (min A) c= (Y1 \/ X1) /\ (Y1 \/ X2) by A7, XBOOLE_1:27;

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

then min A c= Y2 \/ X1 ;

then A9: min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) by A8, XBOOLE_1:19;

( Y1 c= max A & X1 c= max A ) by A3, A4, Th28;

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

then ( min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) & ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) c= max A ) by XBOOLE_1:16;

then A10: ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) in A by Th28;

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

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