let X be set ; 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; UNION ((INTERSECTION (A,B)),B) = B
A1:
UNION ((INTERSECTION (A,B)),B) c= B
proof
let x be
object ;
TARSKI:def 3 ( 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)
;
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;
verum
end;
B c= UNION ((INTERSECTION (A,B)),B)
proof
let x be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;
hence
UNION ((INTERSECTION (A,B)),B) = B
by A1; verum