let X be set ; :: thesis: for A, B being non empty ordered Subset-Family of X holds UNION ((INTERSECTION (A,B)),B) = B
let A, B be non empty ordered Subset-Family of X; :: thesis: UNION ((INTERSECTION (A,B)),B) = B
A1: UNION ((INTERSECTION (A,B)),B) c= B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UNION ((INTERSECTION (A,B)),B) or x in B )
reconsider xx = x as set by TARSKI:1;
set B1 = min B;
set B2 = max B;
assume x in UNION ((INTERSECTION (A,B)),B) ; :: thesis: x in B
then consider Y, Z being set such that
A2: ( Y in INTERSECTION (A,B) & Z in B & x = Y \/ Z ) by SETFAM_1:def 4;
consider Y1, Y2 being set such that
A3: ( Y1 in A & Y2 in B & Y = Y1 /\ Y2 ) by ;
( min B c= Y2 & Y2 c= max B & Y1 /\ Y2 c= Y2 ) by ;
then A4: Y1 /\ Y2 c= max B ;
Z c= max B by ;
then A5: xx c= max B by ;
( min B c= Z & Z c= xx ) by ;
then ( min B c= xx & xx c= max B ) by A5;
hence x in B by Th28; :: thesis: verum
end;
B c= UNION ((INTERSECTION (A,B)),B)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in UNION ((INTERSECTION (A,B)),B) )
reconsider xx = x as set by TARSKI:1;
assume A6: x in B ; :: thesis: x in UNION ((INTERSECTION (A,B)),B)
set b = the Element of A;
A7: x = xx \/ (xx /\ the Element of A) by XBOOLE_1:22;
the Element of A /\ xx in INTERSECTION (A,B) by ;
hence x in UNION ((INTERSECTION (A,B)),B) by ; :: thesis: verum
end;
hence UNION ((INTERSECTION (A,B)),B) = B by A1; :: thesis: verum