let S be Subset-Family of REAL; :: thesis: ( 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 } ; :: thesis: ( 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 ; :: thesis: ( S is semi-diff-closed & S is cap-closed )
now :: thesis: 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 \ B
let A, B be set ; :: thesis: ( 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 ) ; :: thesis: ex F being disjoint_valued FinSequence of S st Union b3 = F \ b2
then 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 ; :: thesis: ex F being disjoint_valued FinSequence of S st Union b3 = F \ b2
then 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; :: thesis: Union F = A \ B
rng F = {K,L} by FINSEQ_2:127;
hence Union F = A \ B by A3, A4, A5, ZFMISC_1:75; :: thesis: verum
end;
suppose A13: I misses J ; :: thesis: ex F being disjoint_valued FinSequence of S st Union b3 = F \ b2
set F = <*I*>;
{I} c= S by A2, A3, ZFMISC_1:31;
then ( dom <*I*> = Seg 1 & rng <*I*> c= S ) by FINSEQ_1:38;
then reconsider F = <*I*> as FinSequence of S by FINSEQ_1:def 4;
reconsider F = F as disjoint_valued FinSequence of S by TTT1;
take F = F; :: thesis: Union F = A \ B
rng F = {I} by FINSEQ_1:38;
hence Union F = A \ B by A13, A3, A4, XBOOLE_1:83; :: thesis: verum
end;
end;
end;
hence S is semi-diff-closed ; :: thesis: S is cap-closed
now :: thesis: for A, B being set st A in S & B in S holds
A /\ B in S
let A, B be set ; :: thesis: ( A in S & B in S implies A /\ B in S )
assume B2: ( A in S & B in S ) ; :: thesis: A /\ B in S
then consider I being Subset of REAL such that
B3: ( A = I & I is right_open_interval ) by A1;
consider J being Subset of REAL such that
B4: ( B = J & J is right_open_interval ) by A1, B2;
I /\ J is right_open_interval by B3, B4, INTERVAL03;
hence A /\ B in S by A1, B3, B4; :: thesis: verum
end;
hence S is cap-closed ; :: thesis: verum