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

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

B c= UNION ((INTERSECTION (A,B)),B)
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 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 ;

Z c= max B by A2, Th28;

then A5: xx c= max B by A2, A3, A4, XBOOLE_1:8;

( min B c= Z & Z c= xx ) by A2, Th28, XBOOLE_1:7;

then ( min B c= xx & xx c= max B ) by A5;

hence x in B by Th28; :: thesis: verum

end;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 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 ;

Z c= max B by A2, Th28;

then A5: xx c= max B by A2, A3, A4, XBOOLE_1:8;

( min B c= Z & Z c= xx ) by A2, Th28, XBOOLE_1:7;

then ( min B c= xx & xx c= max B ) by A5;

hence x in B by Th28; :: thesis: verum

proof

hence
UNION ((INTERSECTION (A,B)),B) = B
by A1; :: thesis: verum
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 A6, SETFAM_1:def 5;

hence x in UNION ((INTERSECTION (A,B)),B) by A7, A6, SETFAM_1:def 4; :: thesis: verum

end;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 A6, SETFAM_1:def 5;

hence x in UNION ((INTERSECTION (A,B)),B) by A7, A6, SETFAM_1:def 4; :: thesis: verum