let S be Subset-Family of REAL; :: thesis: ( S = { s where s is Subset of REAL : s is left_open_interval } implies S is with_countable_Cover )
assume A1: S = { s where s is Subset of REAL : s is left_open_interval } ; :: thesis: S is with_countable_Cover
defpred S₁[ object , object ] means ( $1 is Element of NAT & $2 in S & ex x being real number st
( x = $1 & $2 = ].-infty,x.] ) );
A2: for x being object st x in NAT holds
ex y being object st
( y in S & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in S & S₁[x,y] ) )
assume A3: x in NAT ; :: thesis: ex y being object st
( y in S & S₁[x,y] )
then reconsider x = x as real number ;
set y = ].-infty,x.];
A4: ( ].-infty,x.] is Subset of REAL & ].-infty,x.] is left_open_interval ) by MEASURE5:def 5;
S₁[x,].-infty,x.]] by A1, A3, A4;
hence ex y being object st
( y in S & S₁[x,y] ) ; :: thesis: verum

end;

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

proof

reconsider f = f as SetSequence of REAL by A5, A7, 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 (rng f) = REAL

proof

A9: union (rng f) c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng f) or x in REAL )
assume x in union (rng f) ; :: thesis: x in REAL
then x in Union f ;
then consider t being object such that
A10: ( t in dom f & x in f . t ) by CARD_5:2;
consider x0 being real number such that
A11: ( x0 = t & f . t = ].-infty,x0.] ) by A5, A6, A10;
thus x in REAL by A10, A11; :: thesis: verum

end;

REAL c= union (rng f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL or x in union (rng f) )
assume x in REAL ; :: thesis: x in union (rng f)
then reconsider x = x as Real ;
consider n being Element of NAT such that
A12: x <= n by MESFUNC1:8;
x in f . n

proof

ex z being real number st
( z = n & f . n = ].-infty,z.] ) by A6;
hence x in f . n by A12, XXREAL_1:234; :: thesis: verum

end;

then ( x in f . n & f . n in rng f ) by A5, FUNCT_1:def 3;
hence x in union (rng f) by TARSKI:def 4; :: thesis: verum

end;

hence union (rng f) = REAL by A9; :: thesis: verum

end;

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

end;

hence S is with_countable_Cover by A5, A8, SRINGS_1:def 4; :: thesis: verum