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
proof
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 ;
A4: x = (Y /\ Z1) \/ (Y /\ Z2) by ;
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 ;
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 ;
hence x in A by Th28, A4, A7; :: thesis: verum
end;
A c= INTERSECTION (A,(UNION (A,B)))
proof
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 ;
hence x in INTERSECTION (A,(UNION (A,B))) by ; :: thesis: verum
end;
hence INTERSECTION (A,(UNION (A,B))) = A by A1; :: thesis: verum