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 b₁ being Element of bool (bool the carrier of T) st
( b₁ c= U & b₁ is Cover of the carrier of T & b₁ is countable ) )
assume that
A1: U is open and
A2: U is Cover of T ; :: thesis: ex b₁ being Element of bool (bool the carrier of T) st
( b₁ c= U & b₁ is Cover of the carrier of T & b₁ is countable )

per cases ( the carrier of T = {} or the carrier of T <> {} ) ;

suppose A3: the carrier of T = {} ; :: thesis: ex b₁ being Element of bool (bool the carrier of T) st
( b₁ c= U & b₁ is Cover of the carrier of T & b₁ 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 b₁ being Element of bool (bool the carrier of T) st
( b₁ c= U & b₁ is Cover of the carrier of T & b₁ is countable )

A5: card [:RAT,RAT:] c= omega by CARD_3:def 14, CARD_4:7;
set Q = { ].p,r.[ where p, r is Rational : verum } ;
defpred S₁[ 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 [:RAT,RAT:] & S₁[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 [:RAT,RAT:] & S₁[x,y] ) )
assume x in { ].p,r.[ where p, r is Rational : verum } ; :: thesis: ex y being object st
( y in [:RAT,RAT:] & S₁[x,y] )
then consider a, b being Rational such that
A7: x = ].a,b.[ ;
take y = [a,b]; :: thesis: ( y in [:RAT,RAT:] & S₁[x,y] )
( a in RAT & b in RAT ) by RAT_1:def 2;
hence y in [:RAT,RAT:] by ZFMISC_1:def 2; :: thesis: S₁[x,y]
thus S₁[x,y] by A7; :: thesis: verum

end;

consider h being Function of { ].p,r.[ where p, r is Rational : verum } ,[:RAT,RAT:] such that
A8: for x being object st x in { ].p,r.[ where p, r is Rational : verum } holds
S₁[x,h . x] from FUNCT_2:sch 1(A6);
A9: rng h c= [:RAT,RAT:] ;
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 A8, A11;
consider p2, r2 being Rational such that
A16: x2 = ].p2,r2.[ and
A17: h . x2 = [p2,r2] by A8, A12;
( p1 = p2 & r1 = r2 ) by XTUPLE_0:1, A13, A15, A17;
hence x1 = x2 by A14, A16; :: thesis: verum

end;

then card { ].p,r.[ where p, r is Rational : verum } c= card [:RAT,RAT:] by CARD_1:10, A9, A10;
then A18: { ].p,r.[ where p, r is Rational : verum } is countable by CARD_3:def 14, A5, XBOOLE_1:1;
defpred S₂[ 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 & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of T implies ex y being object st
( y in U & S₂[x,y] ) )
assume A20: x in the carrier of T ; :: thesis: ex y being object st
( y in U & S₂[x,y] )
x in union U by SETFAM_1:def 11, A2, A20, TARSKI:def 3;
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 & S₂[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
S₂[x,f . x] from FUNCT_2:sch 1(A19);
A23: U <> {}

proof

assume A24: U = {} ; :: thesis: contradiction
the carrier of T c= union U by A2, SETFAM_1:def 11;
hence contradiction by A24, ZFMISC_1:2, A4; :: thesis: verum

end;

defpred S₃[ 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 } & S₃[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 } & S₃[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 } & S₃[x,y] )
A27: S₂[x,f . x] by A22, A26;
reconsider Ux = f . x as Subset of T by A27;
Ux is open by A27, A1, TOPS_2:def 1;
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 A28, XBOOLE_1:17;
then consider r1 being Real such that
A29: ( r1 > 0 & ].(x - r1),(x + r1).[ c= Vx ) by A27, FRECHET:8, A28, PRE_TOPC:def 2;
set a = x - r1;
set b = x + r1;
A30: x < x + r1 by XREAL_1:29, A29;
x > x - r1 by XREAL_1:44, A29;
then consider p1, p2 being Rational such that
A31: ( x in ].p1,p2.[ & ].p1,p2.[ c= ].(x - r1),(x + r1).[ ) by Th1, A30, XXREAL_1:4;
set q = ].p1,p2.[;
A32: ].p1,p2.[ c= Vx by A29, A31, XBOOLE_1:1;
take ].p1,p2.[ ; :: thesis: ( ].p1,p2.[ in { ].p,r.[ where p, r is Rational : verum } & S₃[x,].p1,p2.[] )
thus ].p1,p2.[ in { ].p,r.[ where p, r is Rational : verum } ; :: thesis: S₃[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 A28, A31, A32, XBOOLE_1:26; :: 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
S₃[x,f1 . x] from FUNCT_2:sch 1(A25);
deffunc H₁( 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
H₁(x) in U

proof

let x be object ; :: thesis: ( x in rng f1 implies H₁(x) in U )
assume A36: x in rng f1 ; :: thesis: H₁(x) in U
f1 " {x} <> {} by A36, FUNCT_1:72;
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 A23, FUNCT_2:def 1;
then H₁(x) in rng f by FUNCT_1:3;
hence H₁(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 = H₁(q) from FUNCT_2:sch 2(A35);
A39: card (rng f1) c= omega by CARD_3:def 14, A18;
A40: dom g = rng f1 by FUNCT_2:def 1, A23;
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 FUNCT_1:def 2, A42, A34;
A44: f1 . x in {(f1 . x)} by TARSKI:def 1;
A45: f1 . x in rng f1 by FUNCT_1:3, A34, A42;
A46: S₃[x,f1 . x] by A33, A42;
set y = the Element of f1 " {(f1 . x)};
A47: f1 " {(f1 . x)} <> {} by A45, A43, A44, RELAT_1:131;
then A48: x in f1 . the Element of f1 " {(f1 . x)} by A46, Lm1;
A49: f . the Element of f1 " {(f1 . x)} = g . (f1 . x) by A38, FUNCT_1:3, A34, A42;
the Element of f1 " {(f1 . x)} in f1 " {(f1 . x)} by A47;
then A50: S₃[ 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 A42, A48, XBOOLE_0:def 4;
g . (f1 . x) in rng g by FUNCT_1:3, A45, A40;
hence x in union G by A51, TARSKI:def 4, A49, A50; :: thesis: verum

end;

thus G is countable by A41, CARD_3:def 14, A39, XBOOLE_1:1; :: thesis: verum

end;

end;