defpred S₁[ object , object ] means ( $1 is Element of NAT & $2 in II & ex x being real number st
( x = $1 & $2 = ].(- x),x.] ) );
A2: for x being object st x in NAT holds
ex y being object st
( y in II & S₁[x,y] )

proof

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

end;

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

proof

reconsider f = f as SetSequence of REAL by A4, A6, 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
A9: ( t in dom f & x in f . t ) by CARD_5:2;
consider x0 being real number such that
A10: ( x0 = t & f . t = ].(- x0),x0.] ) by A4, A5, A9;
thus x in REAL by A9, A10; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL or 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
A11: |.x.| <= n by MESFUNC1:8;
A12: n + 1 is Element of NAT by ORDINAL1:def 12;
x in f . (n + 1)

proof

consider z being real number such that
A13: ( z = n + 1 & f . (n + 1) = ].(- z),z.] ) by A5, A12;
A14: ( - |.x.| <= x & x <= |.x.| & |.x.| <= n ) by A11, ABSVALUE:4;
A15: ( x <= n implies x + 0 <= n + 1 ) by XREAL_1:7;
- (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 A11, ABSVALUE:def 1;
then A16: - n <= - (- x) by XREAL_1:24;
then A17: (- n) - 1 <= x - 1 by XREAL_1:13;
x - 1 <= x - 0 by XREAL_1:13;
then A18: - (n + 1) <= x by A17, XXREAL_0:2;
- (n + 1) < x

proof

not - (n + 1) = x

proof

assume x = - (n + 1) ; :: thesis: contradiction
then (- n) + n <= (- (n + 1)) + n by A16, XREAL_1:7;
hence contradiction ; :: thesis: verum

end;

hence - (n + 1) < x by A18, XXREAL_0:1; :: thesis: verum

end;

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

end;

end;

end;

hence x in f . (n + 1) by A13, A14, A15, XXREAL_0:2; :: thesis: verum

end;

then ( x in f . (n + 1) & f . (n + 1) in rng f ) by A4, A12, FUNCT_1:def 3;
hence x in Union f by TARSKI:def 4; :: thesis: verum

end;

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

end;

hence II is with_countable_Cover by A4, A7, SRINGS_1:def 4; :: thesis: verum