thus the_set_of_all_open_real_bounded_intervals is cap-closed :: thesis:

proof

now :: thesis:

let x, y be set ; :: thesis:
assume that
A1: x in the_set_of_all_open_real_bounded_intervals and
A2: y in the_set_of_all_open_real_bounded_intervals ; :: thesis:
consider a1, b1 being Real such that
A3: x = ].a1,b1.[ by A1;
consider a2, b2 being Real such that
A4: y = ].a2,b2.[ by A2;
].a1,b1.[ /\ ].a2,b2.[ = ].(max (a1,a2)),(min (b1,b2)).[ by XXREAL_1:142;
hence x /\ y in the_set_of_all_open_real_bounded_intervals by A3, A4; :: thesis:

end;

hence the_set_of_all_open_real_bounded_intervals is cap-closed by FINSUB_1:def 2; :: thesis:

end;

].1,0.[ = {} by XXREAL_1:28;
then {} in the_set_of_all_open_real_bounded_intervals ;
hence the_set_of_all_open_real_bounded_intervals is with_empty_element ; :: thesis:
ex XX being countable Subset of the_set_of_all_open_real_bounded_intervals st XX is Cover of REAL

proof

defpred S₁[ object , object ] means ( c₁ is Element of NAT & c₂ in the_set_of_all_open_real_bounded_intervals & ex x being real number st
( x = c₁ & c₂ = ].(- x),x.[ ) );
A5: for x being object st x in NAT holds
ex y being object st
( y in the_set_of_all_open_real_bounded_intervals & S₁[x,y] )

proof

let x be object ; :: thesis:
assume A6: x in NAT ; :: thesis:
then reconsider x = x as real number ;
set y = ].(- x),x.[;
( ].(- x),x.[ in the_set_of_all_open_real_bounded_intervals & S₁[x,].(- x),x.[] ) by A6;
hence ex y being object st
( y in the_set_of_all_open_real_bounded_intervals & S₁[x,y] ) ; :: thesis:

end;

consider f being Function such that
A7: ( dom f = NAT & rng f c= the_set_of_all_open_real_bounded_intervals ) and
A8: for x being object st x in NAT holds
S₁[x,f . x] from FUNCT_1:sch 6(A5);
A9: rng f is Subset-Family of REAL by A7, XBOOLE_1:1;
A10: rng f is countable

proof

reconsider f = f as SetSequence of REAL by A7, A9, RELSET_1:4, FUNCT_2:def 1;
rng f is countable by TOPGEN_4:58;
hence rng f is countable ; :: thesis:

end;

rng f is Cover of REAL

proof

Union f = REAL

proof

thus Union f c= REAL :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Union f ; :: thesis:
then consider t being object such that
A11: ( t in dom f & x in f . t ) by CARD_5:2;
consider x0 being real number such that
A12: ( x0 = t & f . t = ].(- x0),x0.[ ) by A7, A8, A11;
thus x in REAL by A11, A12; :: thesis:

end;

for x being object st x in REAL holds
x in Union f

proof

let x be object ; :: thesis:
assume x in REAL ; :: thesis:
then reconsider x = x as Real ;
consider n being Element of NAT such that
A13: |.x.| <= n by MESFUNC1:8;
consider z being real number such that
A14: ( z = n + 1 & f . (n + 1) = ].(- z),z.[ ) by A8;
A15: ( - n <= x & x <= n ) by A13, ABSVALUE:5;
(- n) - 1 < - n by XREAL_1:146;
then ( - (n + 1) < x & x < n + 1 ) by A15, XXREAL_0:2, XREAL_1:145;
then ( x in f . (n + 1) & f . (n + 1) in rng f ) by A14, A7, FUNCT_1:def 3, XXREAL_1:4;
hence x in Union f by TARSKI:def 4; :: thesis:

end;

hence REAL c= Union f ; :: thesis:

end;

hence rng f is Cover of REAL by A9, SETFAM_1:45; :: thesis:

end;

hence ex XX being countable Subset of the_set_of_all_open_real_bounded_intervals st XX is Cover of REAL by A7, A10; :: thesis:

end;

hence the_set_of_all_open_real_bounded_intervals is with_countable_Cover by SRINGS_1:def 4; :: thesis: