let S be Subset-Family of REAL; ( S = { I where I is Subset of REAL : I is right_open_interval } implies ( S is with_empty_element & S is semi-diff-closed & S is cap-closed ) )
assume A1:
S = { I where I is Subset of REAL : I is right_open_interval }
; ( S is with_empty_element & S is semi-diff-closed & S is cap-closed )
0 in REAL
by NUMBERS:19;
then
[.0,0.[ is right_open_interval
by NUMBERS:31;
then
{} in S
by A1;
hence
S is with_empty_element
; ( S is semi-diff-closed & S is cap-closed )
now for A, B being set st A in S & B in S holds
ex F being disjoint_valued FinSequence of S st Union F = A \ Blet A,
B be
set ;
( A in S & B in S implies ex F being disjoint_valued FinSequence of S st Union b3 = F \ b2 )assume A2:
(
A in S &
B in S )
;
ex F being disjoint_valued FinSequence of S st Union b3 = F \ b2then consider I being
Subset of
REAL such that A3:
(
A = I &
I is
right_open_interval )
by A1;
consider J being
Subset of
REAL such that A4:
(
B = J &
J is
right_open_interval )
by A1, A2;
per cases
( I meets J or I misses J )
;
suppose
I meets J
;
ex F being disjoint_valued FinSequence of S st Union b3 = F \ b2then consider K,
L being
Subset of
REAL such that A5:
(
K is
right_open_interval &
L is
right_open_interval &
K misses L &
I \ J = K \/ L )
by A3, A4, INTERVAL02;
set F =
<*K,L*>;
(
K in S &
L in S )
by A1, A5;
then
{K,L} c= S
by ZFMISC_1:32;
then
rng <*K,L*> c= S
by FINSEQ_2:127;
then reconsider F =
<*K,L*> as
FinSequence of
S by FINSEQ_1:def 4;
reconsider F =
F as
disjoint_valued FinSequence of
S by A5, Disjoint2;
take F =
F;
Union F = A \ B
rng F = {K,L}
by FINSEQ_2:127;
hence
Union F = A \ B
by A3, A4, A5, ZFMISC_1:75;
verum end; end; end;
hence
S is semi-diff-closed
; S is cap-closed
hence
S is cap-closed
; verum