thus the_set_of_all_closed_real_bounded_intervals is cap-closed :: thesis: ( the_set_of_all_closed_real_bounded_intervals is with_empty_element & the_set_of_all_closed_real_bounded_intervals is with_countable_Cover )

proof

now :: thesis: for x, y being set st x in the_set_of_all_closed_real_bounded_intervals & y in the_set_of_all_closed_real_bounded_intervals holds
x /\ y in the_set_of_all_closed_real_bounded_intervals

let x, y be set ; :: thesis: ( x in the_set_of_all_closed_real_bounded_intervals & y in the_set_of_all_closed_real_bounded_intervals implies x /\ y in the_set_of_all_closed_real_bounded_intervals )
assume that
A1: x in the_set_of_all_closed_real_bounded_intervals and
A2: y in the_set_of_all_closed_real_bounded_intervals ; :: thesis: x /\ y in the_set_of_all_closed_real_bounded_intervals
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:140;
hence x /\ y in the_set_of_all_closed_real_bounded_intervals by A3, A4; :: thesis: verum

end;

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

end;

[.1,0.] = {} by XXREAL_1:29;
then {} in the_set_of_all_closed_real_bounded_intervals ;
hence the_set_of_all_closed_real_bounded_intervals is with_empty_element ; :: thesis: the_set_of_all_closed_real_bounded_intervals is with_countable_Cover
ex XX being countable Subset of the_set_of_all_closed_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_closed_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_closed_real_bounded_intervals & S₁[x,y] )

proof

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

end;

consider f being Function such that
A7: ( dom f = NAT & rng f c= the_set_of_all_closed_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: verum

end;

rng f is Cover of REAL

proof

Union f = REAL

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union f or x in REAL )
assume x in Union f ; :: thesis: x in REAL
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: verum

end;

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

proof

let x be object ; :: thesis: ( x in REAL implies x in Union f )
assume x in REAL ; :: thesis: x in Union f
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 & f . n = [.(- z),z.] ) by A8;
( - n <= x & x <= n ) by A13, ABSVALUE:5;
then ( x in f . n & f . n in rng f ) by A14, XXREAL_1:1, A7, FUNCT_1:def 3;
hence x in Union f by TARSKI:def 4; :: thesis: verum

end;

hence REAL c= Union f ; :: thesis: verum

end;

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

end;

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

end;

hence the_set_of_all_closed_real_bounded_intervals is with_countable_Cover by SRINGS_1:def 4; :: thesis: verum