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_{1} being Element of bool (bool the carrier of T) st

( b_{1} c= U & b_{1} is Cover of the carrier of T & b_{1} is countable ) )

assume that

A1: U is open and

A2: U is Cover of T ; :: thesis: ex b_{1} being Element of bool (bool the carrier of T) st

( b_{1} c= U & b_{1} is Cover of the carrier of T & b_{1} is countable )

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

( b

assume that

A1: U is open and

A2: U is Cover of T ; :: thesis: ex b

( b

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

end;

suppose A3:
the carrier of T = {}
; :: thesis: ex b_{1} being Element of bool (bool the carrier of T) st

( b_{1} c= U & b_{1} is Cover of the carrier of T & b_{1} is countable )

( b

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

end;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

thus
G is countable
; :: thesis: verum
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;assume x in the carrier of T ; :: thesis: x in union G

hence x in union G by A3; :: thesis: verum

suppose A4:
the carrier of T <> {}
; :: thesis: ex b_{1} being Element of bool (bool the carrier of T) st

( b_{1} c= U & b_{1} is Cover of the carrier of T & b_{1} is countable )

( b

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_{1}[ 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_{1}[x,y] )

A8: for x being object st x in { ].p,r.[ where p, r is Rational : verum } holds

S_{1}[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

then A18: { ].p,r.[ where p, r is Rational : verum } is countable by CARD_3:def 14, A5, XBOOLE_1:1;

defpred S_{2}[ 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_{2}[x,y] )

A22: for x being object st x in the carrier of T holds

S_{2}[x,f . x]
from FUNCT_2:sch 1(A19);

A23: U <> {}_{3}[ 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_{3}[x,y] )

A33: for x being object st x in the carrier of T holds

S_{3}[x,f1 . x]
from FUNCT_2:sch 1(A25);

deffunc H_{1}( 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_{1}(x) in U

A38: for q being object st q in rng f1 holds

g . q = H_{1}(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

end;set Q = { ].p,r.[ where p, r is Rational : verum } ;

defpred S

( $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

proof

consider h being Function of { ].p,r.[ where p, r is Rational : verum } ,[:RAT,RAT:] such that
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_{1}[x,y] ) )

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

( y in [:RAT,RAT:] & S_{1}[x,y] )

then consider a, b being Rational such that

A7: x = ].a,b.[ ;

take y = [a,b]; :: thesis: ( y in [:RAT,RAT:] & S_{1}[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_{1}[x,y]

thus S_{1}[x,y]
by A7; :: thesis: verum

end;( y in [:RAT,RAT:] & S

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

( y in [:RAT,RAT:] & S

then consider a, b being Rational such that

A7: x = ].a,b.[ ;

take y = [a,b]; :: thesis: ( y in [:RAT,RAT:] & S

( a in RAT & b in RAT ) by RAT_1:def 2;

hence y in [:RAT,RAT:] by ZFMISC_1:def 2; :: thesis: S

thus S

A8: for x being object st x in { ].p,r.[ where p, r is Rational : verum } holds

S

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

then
card { ].p,r.[ where p, r is Rational : verum } c= card [:RAT,RAT:]
by CARD_1:10, A9, A10;
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;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

then A18: { ].p,r.[ where p, r is Rational : verum } is countable by CARD_3:def 14, A5, XBOOLE_1:1;

defpred S

( 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

proof

consider f being Function of the carrier of T,U such that
let x be object ; :: thesis: ( x in the carrier of T implies ex y being object st

( y in U & S_{2}[x,y] ) )

assume A20: x in the carrier of T ; :: thesis: ex y being object st

( y in U & S_{2}[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_{2}[x,y] )
by A21; :: thesis: verum

end;( y in U & S

assume A20: x in the carrier of T ; :: thesis: ex y being object st

( y in U & S

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

A22: for x being object st x in the carrier of T holds

S

A23: U <> {}

proof

defpred S
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;the carrier of T c= union U by A2, SETFAM_1:def 11;

hence contradiction by A24, ZFMISC_1:2, A4; :: thesis: verum

( 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

proof

consider f1 being Function of the carrier of T, { ].p,r.[ where p, r is Rational : verum } such that
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_{3}[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_{3}[x,y] )

A27: S_{2}[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_{3}[x,].p1,p2.[] )

thus ].p1,p2.[ in { ].p,r.[ where p, r is Rational : verum } ; :: thesis: S_{3}[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;( y in { ].p,r.[ where p, r is Rational : verum } & S

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

A27: S

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

thus ].p1,p2.[ in { ].p,r.[ where p, r is Rational : verum } ; :: thesis: S

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

A33: for x being object st x in the carrier of T holds

S

deffunc H

].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

proof

consider g being Function of (rng f1),U such that
let x be object ; :: thesis: ( x in rng f1 implies H_{1}(x) in U )

assume A36: x in rng f1 ; :: thesis: H_{1}(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_{1}(x) in rng f
by FUNCT_1:3;

hence H_{1}(x) in U
; :: thesis: verum

end;assume A36: x in rng f1 ; :: thesis: H

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

hence H

A38: for q being object st q in rng f1 holds

g . q = H

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

thus
G is countable
by A41, CARD_3:def 14, A39, XBOOLE_1:1; :: thesis: verum
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_{3}[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_{3}[ 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;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

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

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