let X be set ; for A, B being non empty ordered Subset-Family of X holds INTERSECTION (A,(UNION (A,B))) = A
let A, B be non empty ordered Subset-Family of X; INTERSECTION (A,(UNION (A,B))) = A
set A1 = min A;
set A2 = max A;
A1:
INTERSECTION (A,(UNION (A,B))) c= A
proof
let x be
object ;
TARSKI:def 3 ( not x in INTERSECTION (A,(UNION (A,B))) or x in A )
assume
x in INTERSECTION (
A,
(UNION (A,B)))
;
x in A
then consider Y,
Z being
set such that A2:
(
Y in A &
Z in UNION (
A,
B) &
x = Y /\ Z )
by SETFAM_1:def 5;
consider Z1,
Z2 being
set such that A3:
(
Z1 in A &
Z2 in B &
Z = Z1 \/ Z2 )
by A2, SETFAM_1:def 4;
A4:
x = (Y /\ Z1) \/ (Y /\ Z2)
by A2, A3, XBOOLE_1:23;
A5:
(
min A c= Y &
Y c= max A &
min A c= Z1 &
Z1 c= max A )
by Th28, A2, A3;
then
(
min A c= Y /\ Z1 &
Y /\ Z1 c= (max A) /\ (max A) )
by XBOOLE_1:19, XBOOLE_1:27;
then A6:
(
min A c= Y /\ Z1 &
Y /\ Z1 c= max A &
Y /\ Z1 c= (Y /\ Z1) \/ (Y /\ Z2) )
by XBOOLE_1:7;
then A7:
min A c= (Y /\ Z1) \/ (Y /\ Z2)
;
Y /\ Z2 c= Y
by XBOOLE_1:17;
then
Y /\ Z2 c= max A
by A5;
then
(Y /\ Z1) \/ (Y /\ Z2) c= max A
by A6, XBOOLE_1:8;
hence
x in A
by Th28, A4, A7;
verum
end;
A c= INTERSECTION (A,(UNION (A,B)))
proof
let x be
object ;
TARSKI:def 3 ( not x in A or x in INTERSECTION (A,(UNION (A,B))) )
reconsider xx =
x as
set by TARSKI:1;
assume A8:
x in A
;
x in INTERSECTION (A,(UNION (A,B)))
set b = the
Element of
B;
A9:
x = xx /\ (xx \/ the Element of B)
by XBOOLE_1:21;
xx \/ the
Element of
B in UNION (
A,
B)
by A8, SETFAM_1:def 4;
hence
x in INTERSECTION (
A,
(UNION (A,B)))
by A8, A9, SETFAM_1:def 5;
verum
end;
hence
INTERSECTION (A,(UNION (A,B))) = A
by A1; verum