set S = { I where I is Interval : verum } ;
now :: thesis: for A being object st A in { I where I is Interval : verum } holds
A in bool REAL
let A be object ; :: thesis: ( A in { I where I is Interval : verum } implies A in bool REAL )
assume A in { I where I is Interval : verum } ; :: thesis: A in bool REAL
then consider I being Interval such that
A2: A = I ;
thus A in bool REAL by A2; :: thesis: verum
end;
then { I where I is Interval : verum } c= bool REAL ;
then reconsider S = { I where I is Interval : verum } as Subset-Family of REAL ;
{} c= REAL ;
then reconsider E = {} as Subset of REAL ;
A3: E in S ;
then A4: S is with_empty_element ;
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 A5: ( A in S & B in S ) ; :: thesis: ex F being disjoint_valued FinSequence of S st Union b3 = F \ b2
then consider I being Interval such that
A6: A = I ;
consider J being Interval such that
A7: B = J by A5;
per cases ( I misses J or I meets J ) ;
suppose A8: I misses J ; :: thesis: ex F being disjoint_valued FinSequence of S st Union b3 = F \ b2
set F = <*A*>;
A9: rng <*A*> = {A} by FINSEQ_1:38;
then reconsider F = <*A*> as FinSequence of S by A5, ZFMISC_1:31, FINSEQ_1:def 4;
reconsider F = F as disjoint_valued FinSequence of S by TTT1;
take F = F; :: thesis: Union F = A \ B
thus Union F = A \ B by A6, A8, A7, XBOOLE_1:83, A9; :: thesis: verum
end;
suppose A10: I meets J ; :: thesis: ex F being disjoint_valued FinSequence of S st Union b3 = F \ b2
( ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) & ( J is open_interval or J is closed_interval or J is right_open_interval or J is left_open_interval ) ) by MEASURE5:1;
then consider K, L being Interval such that
A11: ( K misses L & I \ J = K \/ L ) by A10, OOdif, OCdif, ORdif, OLdif, COdif, CCdif, CRdif, CLdif, ROdif, RCdif, RRdif, RLdif, LOdif, LCdif, LRdif, LLdif;
set F = <*K,L*>;
( K in S & L in S ) ;
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 A11, Disjoint2;
take F = F; :: thesis: Union F = A \ B
rng F = {K,L} by FINSEQ_2:127;
hence Union F = A \ B by A6, A7, A11, ZFMISC_1:75; :: thesis: verum
end;
end;
end;
then P2: S is semi-diff-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 b1 /\ b2 in S )
assume A12: ( A in S & B in S ) ; :: thesis: b1 /\ b2 in S
then consider I being Interval such that
A13: A = I ;
consider J being Interval such that
A14: B = J by A12;
per cases ( I misses J or I meets J ) ;
suppose I misses J ; :: thesis: b1 /\ b2 in S
hence A /\ B in S by A3, A13, A14; :: thesis: verum
end;
end;
end;
then P3: S is cap-closed ;
reconsider R = ].-infty,+infty.[ as Subset of REAL ;
R is open_interval ;
then REAL in S by XXREAL_1:224;
hence { I where I is Interval : verum } is semialgebra_of_sets of REAL by A4, P2, P3, Def1; :: thesis: verum