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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in UNION ((INTERSECTION (A,B)),B) or x in B )
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 A2, SETFAM_1:def 5;
( min B c= Y2 & Y2 c= max B & Y1 /\ Y2 c= Y2 ) by A3, Th28, XBOOLE_1:17;
then A4: Y1 /\ Y2 c= max B by XBOOLE_1:1;
Z c= max B by A2, Th28;
then A5: x c= max B by A2, A3, A4, XBOOLE_1:8;
( min B c= Z & Z c= x ) by A2, Th28, XBOOLE_1:7;
then ( min B c= x & x c= max B ) by A5, XBOOLE_1:1;
hence x in B by Th28; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in UNION ((INTERSECTION (A,B)),B) )
assume A6: x in B ; :: thesis: x in UNION ((INTERSECTION (A,B)),B)
set b = the Element of A;
A7: x = x \/ (x /\ the Element of A) by XBOOLE_1:22;
the Element of A /\ x in INTERSECTION (A,B) by A6, SETFAM_1:def 5;
hence x in UNION ((INTERSECTION (A,B)),B) by A7, A6, SETFAM_1:def 4; :: thesis: verum

end;

hence UNION ((INTERSECTION (A,B)),B) = B by A1, XBOOLE_0:def 10; :: thesis: verum