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
set ;
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 a3:
(
Y in A &
Z in UNION A,
B &
x = Y /\ Z )
by SETFAM_1:def 5;
consider Z1,
Z2 being
set such that a4:
(
Z1 in A &
Z2 in B &
Z = Z1 \/ Z2 )
by SETFAM_1:def 4, a3;
a5:
x = (Y /\ Z1) \/ (Y /\ Z2)
by XBOOLE_1:23, a3, a4;
a8:
(
min A c= Y &
Y c= max A &
min A c= Z1 &
Z1 c= max A )
by Nowe1, a3, a4;
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)
by XBOOLE_1:1;
Y /\ Z2 c= Y
by XBOOLE_1:17;
then
Y /\ Z2 c= max A
by a8, XBOOLE_1:1;
then
(Y /\ Z1) \/ (Y /\ Z2) c= max A
by XBOOLE_1:8, a6;
hence
x in A
by Nowe1, a5, a7;
verum
end;
A c= INTERSECTION A,(UNION A,B)
proof
let x be
set ;
TARSKI:def 3 ( not x in A or x in INTERSECTION A,(UNION A,B) )
assume b0:
x in A
;
x in INTERSECTION A,(UNION A,B)
consider b being
Element of
B;
L1:
x = x /\ (x \/ b)
by XBOOLE_1:21;
x \/ b in UNION A,
B
by b0, SETFAM_1:def 4;
hence
x in INTERSECTION A,
(UNION A,B)
by b0, L1, SETFAM_1:def 5;
verum
end;
hence
INTERSECTION A,(UNION A,B) = A
by a1, XBOOLE_0:def 10; verum