let T be SubSpace of R^1 ; :: thesis: T is Lindelof
let U be Subset-Family of T; :: according to METRIZTS:def 2 :: thesis: ( not U is open or not U is Cover of the carrier of T or ex b1 being Element of bool (bool the carrier of T) st
( b1 c= U & b1 is Cover of the carrier of T & b1 is countable ) )

assume that
A1: U is open and
A2: U is Cover of T ; :: thesis: ex b1 being Element of bool (bool the carrier of T) st
( b1 c= U & b1 is Cover of the carrier of T & b1 is countable )

per cases ( the carrier of T = {} or the carrier of T <> {} ) ;
suppose A3: the carrier of T = {} ; :: thesis: ex b1 being Element of bool (bool the carrier of T) st
( b1 c= U & b1 is Cover of the carrier of T & b1 is countable )

reconsider G = {} as Subset-Family of T by XBOOLE_1:2;
take G ; :: thesis: ( G c= U & G is Cover of the carrier of T & G is countable )
thus G c= U by XBOOLE_1:2; :: thesis: ( G is Cover of the carrier of T & G is countable )
thus G is Cover of T :: thesis: G is countable
proof
let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not x in the carrier of T or x in union G )
assume x in the carrier of T ; :: thesis: x in union G
hence x in union G by A3; :: thesis: verum
end;
thus G is countable ; :: thesis: verum
end;
suppose A4: the carrier of T <> {} ; :: thesis: ex b1 being Element of bool (bool the carrier of T) st
( b1 c= U & b1 is Cover of the carrier of T & b1 is countable )

A5: card c= omega by ;
set Q = { ].p,r.[ where p, r is Rational : verum } ;
defpred S1[ object , object ] means ex a, b being Rational st
( \$1 = ].a,b.[ & \$2 = [a,b] );
A6: for x being object st x in { ].p,r.[ where p, r is Rational : verum } holds
ex y being object st
( y in & S1[x,y] )
proof
let x be object ; :: thesis: ( x in { ].p,r.[ where p, r is Rational : verum } implies ex y being object st
( y in & S1[x,y] ) )

assume x in { ].p,r.[ where p, r is Rational : verum } ; :: thesis: ex y being object st
( y in & S1[x,y] )

then consider a, b being Rational such that
A7: x = ].a,b.[ ;
take y = [a,b]; :: thesis: ( y in & S1[x,y] )
( a in RAT & b in RAT ) by RAT_1:def 2;
hence y in by ZFMISC_1:def 2; :: thesis: S1[x,y]
thus S1[x,y] by A7; :: thesis: verum
end;
consider h being Function of { ].p,r.[ where p, r is Rational : verum } , such that
A8: for x being object st x in { ].p,r.[ where p, r is Rational : verum } holds
S1[x,h . x] from A9: rng h c= ;
A10: dom h = { ].p,r.[ where p, r is Rational : verum } by FUNCT_2:def 1;
h is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom h or not x2 in dom h or not h . x1 = h . x2 or x1 = x2 )
assume that
A11: x1 in dom h and
A12: x2 in dom h and
A13: h . x1 = h . x2 ; :: thesis: x1 = x2
consider p1, r1 being Rational such that
A14: x1 = ].p1,r1.[ and
A15: h . x1 = [p1,r1] by ;
consider p2, r2 being Rational such that
A16: x2 = ].p2,r2.[ and
A17: h . x2 = [p2,r2] by ;
( p1 = p2 & r1 = r2 ) by ;
hence x1 = x2 by ; :: thesis: verum
end;
then card { ].p,r.[ where p, r is Rational : verum } c= card by ;
then A18: { ].p,r.[ where p, r is Rational : verum } is countable by ;
defpred S2[ object , object ] means ex S being set st
( S = \$2 & \$1 in S & \$2 in U );
A19: for x being object st x in the carrier of T holds
ex y being object st
( y in U & S2[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of T implies ex y being object st
( y in U & S2[x,y] ) )

assume A20: x in the carrier of T ; :: thesis: ex y being object st
( y in U & S2[x,y] )

x in union U by ;
then consider Ux being set such that
A21: ( x in Ux & Ux in U ) by TARSKI:def 4;
thus ex y being object st
( y in U & S2[x,y] ) by A21; :: thesis: verum
end;
consider f being Function of the carrier of T,U such that
A22: for x being object st x in the carrier of T holds
S2[x,f . x] from A23: U <> {}
proof
assume A24: U = {} ; :: thesis: contradiction
the carrier of T c= union U by ;
hence contradiction by A24, ZFMISC_1:2, A4; :: thesis: verum
end;
defpred S3[ object , object ] means ex S being set st
( S = \$2 & \$2 in { ].p,r.[ where p, r is Rational : verum } & \$1 in S & S /\ ([#] T) c= f . \$1 );
A25: for x being object st x in the carrier of T holds
ex y being object st
( y in { ].p,r.[ where p, r is Rational : verum } & S3[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of T implies ex y being object st
( y in { ].p,r.[ where p, r is Rational : verum } & S3[x,y] ) )

assume A26: x in the carrier of T ; :: thesis: ex y being object st
( y in { ].p,r.[ where p, r is Rational : verum } & S3[x,y] )

A27: S2[x,f . x] by ;
reconsider Ux = f . x as Subset of T by A27;
Ux is open by ;
then consider Vx being Subset of R^1 such that
A28: ( Vx in the topology of R^1 & Ux = Vx /\ ([#] T) ) by PRE_TOPC:def 4;
reconsider x = x as Real by A26;
Ux c= Vx by ;
then consider r1 being Real such that
A29: ( r1 > 0 & ].(x - r1),(x + r1).[ c= Vx ) by ;
set a = x - r1;
set b = x + r1;
A30: x < x + r1 by ;
x > x - r1 by ;
then consider p1, p2 being Rational such that
A31: ( x in ].p1,p2.[ & ].p1,p2.[ c= ].(x - r1),(x + r1).[ ) by ;
set q = ].p1,p2.[;
A32: ].p1,p2.[ c= Vx by ;
take ].p1,p2.[ ; :: thesis: ( ].p1,p2.[ in { ].p,r.[ where p, r is Rational : verum } & S3[x,].p1,p2.[] )
thus ].p1,p2.[ in { ].p,r.[ where p, r is Rational : verum } ; :: thesis: S3[x,].p1,p2.[]
take ].p1,p2.[ ; :: thesis: ( ].p1,p2.[ = ].p1,p2.[ & ].p1,p2.[ in { ].p,r.[ where p, r is Rational : verum } & x in ].p1,p2.[ & ].p1,p2.[ /\ ([#] T) c= f . x )
thus ( ].p1,p2.[ = ].p1,p2.[ & ].p1,p2.[ in { ].p,r.[ where p, r is Rational : verum } & x in ].p1,p2.[ & ].p1,p2.[ /\ ([#] T) c= f . x ) by ; :: thesis: verum
end;
consider f1 being Function of the carrier of T, { ].p,r.[ where p, r is Rational : verum } such that
A33: for x being object st x in the carrier of T holds
S3[x,f1 . x] from deffunc H1( object ) -> set = f . the Element of f1 " {\$1};
].2,1.[ in { ].p,r.[ where p, r is Rational : verum } ;
then A34: dom f1 = the carrier of T by FUNCT_2:def 1;
A35: for x being object st x in rng f1 holds
H1(x) in U
proof
let x be object ; :: thesis: ( x in rng f1 implies H1(x) in U )
assume A36: x in rng f1 ; :: thesis: H1(x) in U
f1 " {x} <> {} by ;
then A37: the Element of f1 " {x} in f1 " {x} ;
the Element of f1 " {x} in the carrier of T by A37;
then the Element of f1 " {x} in dom f by ;
then H1(x) in rng f by FUNCT_1:3;
hence H1(x) in U ; :: thesis: verum
end;
consider g being Function of (rng f1),U such that
A38: for q being object st q in rng f1 holds
g . q = H1(q) from A39: card (rng f1) c= omega by ;
A40: dom g = rng f1 by ;
then A41: card (rng g) c= card (rng f1) by CARD_1:12;
reconsider G = rng g as Subset-Family of T by TOPS_2:2;
take G ; :: thesis: ( G c= U & G is Cover of the carrier of T & G is countable )
thus G c= U ; :: thesis: ( G is Cover of the carrier of T & G is countable )
thus G is Cover of T :: thesis: G is countable
proof
let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not x in the carrier of T or x in union G )
assume A42: x in the carrier of T ; :: thesis: x in union G
set q = f1 . x;
A43: [x,(f1 . x)] in f1 by ;
A44: f1 . x in {(f1 . x)} by TARSKI:def 1;
A45: f1 . x in rng f1 by ;
A46: S3[x,f1 . x] by ;
set y = the Element of f1 " {(f1 . x)};
A47: f1 " {(f1 . x)} <> {} by ;
then A48: x in f1 . the Element of f1 " {(f1 . x)} by ;
A49: f . the Element of f1 " {(f1 . x)} = g . (f1 . x) by ;
the Element of f1 " {(f1 . x)} in f1 " {(f1 . x)} by A47;
then A50: S3[ the Element of f1 " {(f1 . x)},f1 . the Element of f1 " {(f1 . x)}] by A33;
A51: x in (f1 . the Element of f1 " {(f1 . x)}) /\ ([#] T) by ;
g . (f1 . x) in rng g by ;
hence x in union G by ; :: thesis: verum
end;
thus G is countable by ; :: thesis: verum
end;
end;