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

let A, B be non empty ordered Subset-Family of X; :: thesis: INTERSECTION (A,(UNION (A,B))) = A

set A1 = min A;

set A2 = max A;

A1: INTERSECTION (A,(UNION (A,B))) c= A

let A, B be non empty ordered Subset-Family of X; :: thesis: INTERSECTION (A,(UNION (A,B))) = A

set A1 = min A;

set A2 = max A;

A1: INTERSECTION (A,(UNION (A,B))) c= A

proof

A c= INTERSECTION (A,(UNION (A,B)))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in INTERSECTION (A,(UNION (A,B))) or x in A )

assume x in INTERSECTION (A,(UNION (A,B))) ; :: thesis: x in A

then consider Y, Z being set such that

A2: ( Y in A & Z in UNION (A,B) & x = Y /\ Z ) by SETFAM_1:def 5;

consider Z1, Z2 being set such that

A3: ( Z1 in A & Z2 in B & Z = Z1 \/ Z2 ) by A2, SETFAM_1:def 4;

A4: x = (Y /\ Z1) \/ (Y /\ Z2) by A2, A3, XBOOLE_1:23;

A5: ( min A c= Y & Y c= max A & min A c= Z1 & Z1 c= max A ) by Th28, A2, A3;

then ( min A c= Y /\ Z1 & Y /\ Z1 c= (max A) /\ (max A) ) by XBOOLE_1:19, XBOOLE_1:27;

then A6: ( min A c= Y /\ Z1 & Y /\ Z1 c= max A & Y /\ Z1 c= (Y /\ Z1) \/ (Y /\ Z2) ) by XBOOLE_1:7;

then A7: min A c= (Y /\ Z1) \/ (Y /\ Z2) ;

Y /\ Z2 c= Y by XBOOLE_1:17;

then Y /\ Z2 c= max A by A5;

then (Y /\ Z1) \/ (Y /\ Z2) c= max A by A6, XBOOLE_1:8;

hence x in A by Th28, A4, A7; :: thesis: verum

end;assume x in INTERSECTION (A,(UNION (A,B))) ; :: thesis: x in A

then consider Y, Z being set such that

A2: ( Y in A & Z in UNION (A,B) & x = Y /\ Z ) by SETFAM_1:def 5;

consider Z1, Z2 being set such that

A3: ( Z1 in A & Z2 in B & Z = Z1 \/ Z2 ) by A2, SETFAM_1:def 4;

A4: x = (Y /\ Z1) \/ (Y /\ Z2) by A2, A3, XBOOLE_1:23;

A5: ( min A c= Y & Y c= max A & min A c= Z1 & Z1 c= max A ) by Th28, A2, A3;

then ( min A c= Y /\ Z1 & Y /\ Z1 c= (max A) /\ (max A) ) by XBOOLE_1:19, XBOOLE_1:27;

then A6: ( min A c= Y /\ Z1 & Y /\ Z1 c= max A & Y /\ Z1 c= (Y /\ Z1) \/ (Y /\ Z2) ) by XBOOLE_1:7;

then A7: min A c= (Y /\ Z1) \/ (Y /\ Z2) ;

Y /\ Z2 c= Y by XBOOLE_1:17;

then Y /\ Z2 c= max A by A5;

then (Y /\ Z1) \/ (Y /\ Z2) c= max A by A6, XBOOLE_1:8;

hence x in A by Th28, A4, A7; :: thesis: verum

proof

hence
INTERSECTION (A,(UNION (A,B))) = A
by A1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in INTERSECTION (A,(UNION (A,B))) )

reconsider xx = x as set by TARSKI:1;

assume A8: x in A ; :: thesis: x in INTERSECTION (A,(UNION (A,B)))

set b = the Element of B;

A9: x = xx /\ (xx \/ the Element of B) by XBOOLE_1:21;

xx \/ the Element of B in UNION (A,B) by A8, SETFAM_1:def 4;

hence x in INTERSECTION (A,(UNION (A,B))) by A8, A9, SETFAM_1:def 5; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume A8: x in A ; :: thesis: x in INTERSECTION (A,(UNION (A,B)))

set b = the Element of B;

A9: x = xx /\ (xx \/ the Element of B) by XBOOLE_1:21;

xx \/ the Element of B in UNION (A,B) by A8, SETFAM_1:def 4;

hence x in INTERSECTION (A,(UNION (A,B))) by A8, A9, SETFAM_1:def 5; :: thesis: verum