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 )
set B1 = min B;
set B2 = max 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