defpred S₁[ object , object ] means ( $1 is Element of NAT & $2 in the_set_of_all_right_open_real_bounded_intervals & ex x being real number st
( x = $1 & $2 = [.(- x),x.[ ) );
A1: for x being object st x in NAT holds
ex y being object st
( y in the_set_of_all_right_open_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_right_open_real_bounded_intervals & S₁[x,y] ) )
assume A2: x in NAT ; :: thesis: ex y being object st
( y in the_set_of_all_right_open_real_bounded_intervals & S₁[x,y] )
then reconsider x = x as real number ;
set y = [.(- x),x.[;
( [.(- x),x.[ in the_set_of_all_right_open_real_bounded_intervals & S₁[x,[.(- x),x.[] ) by A2;
hence ex y being object st
( y in the_set_of_all_right_open_real_bounded_intervals & S₁[x,y] ) ; :: thesis: verum

end;

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

proof

reconsider f = f as SetSequence of REAL by A3, A5, 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
A7: ( t in dom f & x in f . t ) by CARD_5:2;
consider x0 being real number such that
A8: ( x0 = t & f . t = [.(- x0),x0.[ ) by A3, A4, A7;
thus x in REAL by A7, A8; :: 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
A9: |.x.| <= n by MESFUNC1:8;
x in f . (n + 1)

proof

consider z being real number such that
A10: ( z = n + 1 & f . (n + 1) = [.(- z),z.[ ) by A4;
A11: x < n + 1

proof

assume A12: not x < n + 1 ; :: thesis: contradiction
x <= n by A9, ABSVALUE:def 1;
then n + 1 <= n by A12, XXREAL_0:2;
hence contradiction by NAT_1:13; :: thesis: verum

end;

- (n + 1) <= x

proof

per cases ( 0 <= x or x < 0 ) ;

suppose 0 <= x ; :: thesis: - (n + 1) <= x

hence - (n + 1) <= x ; :: thesis: verum

end;

suppose x < 0 ; :: thesis: - (n + 1) <= x

then - x <= n by A9, ABSVALUE:def 1;
then - n <= - (- x) by XREAL_1:24;
then A13: (- n) - 1 <= x - 1 by XREAL_1:13;
x - 1 <= x - 0 by XREAL_1:13;
hence - (n + 1) <= x by A13, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence x in f . (n + 1) by A10, A11, XXREAL_1:3; :: thesis: verum

end;

then ( x in f . (n + 1) & f . (n + 1) in rng f ) by A3, 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 A5, SETFAM_1:45; :: thesis: verum

end;

hence the_set_of_all_right_open_real_bounded_intervals is with_countable_Cover by A3, A6, SRINGS_1:def 4; :: thesis: verum