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
a0: 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 SETFAM_1:def 5, a2;
( min B c= Y2 & Y2 c= max B & Y1 /\ Y2 c= Y2 ) by a3, Nowe1, XBOOLE_1:17;
then a5: Y1 /\ Y2 c= max B by XBOOLE_1:1;
Z c= max B by a2, Nowe1;
then a6: x c= max B by a2, a3, a5, XBOOLE_1:8;
( min B c= Z & Z c= x ) by a2, Nowe1, XBOOLE_1:7;
then ( min B c= x & x c= max B ) by a6, XBOOLE_1:1;
hence x in B by Nowe1; :: 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 a1: x in B ; :: thesis: x in UNION ((INTERSECTION (A,B)),B)
consider b being Element of A;
L1: x = x \/ (x /\ b) by XBOOLE_1:22;
b /\ x in INTERSECTION (A,B) by a1, SETFAM_1:def 5;
hence x in UNION ((INTERSECTION (A,B)),B) by L1, a1, SETFAM_1:def 4; :: thesis: verum

end;

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