set S = Sorgenfrey-line ;

let U be Subset-Family of Sorgenfrey-line; :: according to METRIZTS:def 2 :: thesis: ( not U is open or not U is Cover of the carrier of Sorgenfrey-line or ex b_{1} being Element of bool (bool the carrier of Sorgenfrey-line) st

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

assume that

A1: U is open and

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

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

A3: U <> {}

set W = union { (Int u) where u is Subset of R^1 : u in U } ;

reconsider K = ([#] Sorgenfrey-line) \ (union { (Int u) where u is Subset of R^1 : u in U } ) as set ;

{ (Int u) where u is Subset of R^1 : u in U } is non empty Subset-Family of R^1

union { (Int u) where u is Subset of R^1 : u in U } c= [#] R^1

defpred S_{1}[ object , object ] means ex y being Subset of R^1 st

( $2 = y & y in U & $1 = Int y );

A11: for x being object st x in V holds

ex y being object st

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

A15: for x being object st x in V holds

S_{1}[x,h . x]
from FUNCT_2:sch 1(A11);

A16: for x being Element of V

for hx being Subset of R^1 st hx = h . x holds

x = Int hx

V c= bool ([#] T)

A21: V1 is open

A26: B c= V and

A27: B is Cover of T and

A28: B is countable by METRIZTS:def 2, A21, A25, SETFAM_1:def 11;

deffunc H_{1}( object ) -> set = h . $1;

A29: for x being object st x in B holds

H_{1}(x) in U

A30: for x being object st x in B holds

f . x = H_{1}(x)
from FUNCT_2:sch 2(A29);

reconsider Y = rng f as Subset-Family of Sorgenfrey-line by TOPS_2:2;

A31: Y is Cover of W

dom f = B by FUNCT_2:def 1, A3;

then card (rng f) c= card B by CARD_1:12;

then A39: Y is countable by CARD_3:def 14, A38, XBOOLE_1:1;

defpred S_{2}[ object , object ] means ex S being set st

( S = $2 & $1 in S );

A40: for x being object st x in K holds

ex y being object st

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

A43: for x being object st x in K holds

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

set Q = { [.p,r.[ where p, r is Real : r > p } ;

defpred S_{3}[ object , object ] means ex S being set st

( S = $2 & S c= g . $1 & ex x, rx being Real st

( $1 = x & $2 = [.x,rx.[ ) );

A44: for x being object st x in K holds

ex y being object st

( y in { [.p,r.[ where p, r is Real : r > p } & S_{3}[x,y] )

A53: for x being object st x in K holds

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

defpred S_{4}[ object , object ] means ex S being set st

( S = $1 & $2 in S );

A54: for x being object st x in rng k holds

ex y being object st

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

A59: for x being object st x in rng k holds

S_{4}[x,j . x]
from FUNCT_2:sch 1(A54);

A60: for x, y being Element of Sorgenfrey-line st x in K & y in K & x <> y holds

k . x misses k . y

A83: dom j = rng k by FUNCT_2:def 1;

A84: j is one-to-one

A92: [.1,2.[ in { [.p,r.[ where p, r is Real : r > p } ;

then A93: dom k = K by FUNCT_2:def 1;

A94: k is one-to-one

A104: card K c= omega by A103, A91, XBOOLE_1:1;

dom g = K by FUNCT_2:def 1, A3;

then card (rng g) c= card K by CARD_1:12;

then A105: rng g is countable by CARD_3:def 14, A104, XBOOLE_1:1;

reconsider Z = rng g as Subset-Family of Sorgenfrey-line by TOPS_2:2;

A106: Z is Cover of K

A110: Z \/ Y is Cover of [#] Sorgenfrey-line

take G ; :: thesis: ( G c= U & G is Cover of the carrier of Sorgenfrey-line & G is countable )

thus G c= U by XBOOLE_1:8; :: thesis: ( G is Cover of the carrier of Sorgenfrey-line & G is countable )

thus G is Cover of Sorgenfrey-line by A110; :: thesis: G is countable

thus G is countable by CARD_2:85, A105, A39; :: thesis: verum

let U be Subset-Family of Sorgenfrey-line; :: according to METRIZTS:def 2 :: thesis: ( not U is open or not U is Cover of the carrier of Sorgenfrey-line or ex b

( b

assume that

A1: U is open and

A2: U is Cover of Sorgenfrey-line ; :: thesis: ex b

( b

A3: U <> {}

proof

set V = { (Int u) where u is Subset of R^1 : u in U } ;
assume A4:
U = {}
; :: thesis: contradiction

the carrier of Sorgenfrey-line c= union U by SETFAM_1:def 11, A2;

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

end;the carrier of Sorgenfrey-line c= union U by SETFAM_1:def 11, A2;

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

set W = union { (Int u) where u is Subset of R^1 : u in U } ;

reconsider K = ([#] Sorgenfrey-line) \ (union { (Int u) where u is Subset of R^1 : u in U } ) as set ;

{ (Int u) where u is Subset of R^1 : u in U } is non empty Subset-Family of R^1

proof

then reconsider V = { (Int u) where u is Subset of R^1 : u in U } as non empty Subset-Family of R^1 ;
consider u being object such that

A5: u in U by XBOOLE_0:def 1, A3;

reconsider u = u as Subset of R^1 by TOPGEN_3:def 2, TOPMETR:17, A5;

set v = Int u;

A6: { (Int u) where u is Subset of R^1 : u in U } c= bool ([#] R^1)

hence { (Int u) where u is Subset of R^1 : u in U } is non empty Subset-Family of R^1 by A6; :: thesis: verum

end;A5: u in U by XBOOLE_0:def 1, A3;

reconsider u = u as Subset of R^1 by TOPGEN_3:def 2, TOPMETR:17, A5;

set v = Int u;

A6: { (Int u) where u is Subset of R^1 : u in U } c= bool ([#] R^1)

proof

Int u in { (Int u) where u is Subset of R^1 : u in U }
by A5;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Int u) where u is Subset of R^1 : u in U } or x in bool ([#] R^1) )

assume A7: x in { (Int u) where u is Subset of R^1 : u in U } ; :: thesis: x in bool ([#] R^1)

consider u being Subset of R^1 such that

A8: Int u = x and

u in U by A7;

thus x in bool ([#] R^1) by A8; :: thesis: verum

end;assume A7: x in { (Int u) where u is Subset of R^1 : u in U } ; :: thesis: x in bool ([#] R^1)

consider u being Subset of R^1 such that

A8: Int u = x and

u in U by A7;

thus x in bool ([#] R^1) by A8; :: thesis: verum

hence { (Int u) where u is Subset of R^1 : u in U } is non empty Subset-Family of R^1 by A6; :: thesis: verum

union { (Int u) where u is Subset of R^1 : u in U } c= [#] R^1

proof

then reconsider W = union { (Int u) where u is Subset of R^1 : u in U } as Subset of R^1 ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (Int u) where u is Subset of R^1 : u in U } or x in [#] R^1 )

assume x in union { (Int u) where u is Subset of R^1 : u in U } ; :: thesis: x in [#] R^1

then consider v being set such that

A9: x in v and

A10: v in V by TARSKI:def 4;

thus x in [#] R^1 by A9, A10; :: thesis: verum

end;assume x in union { (Int u) where u is Subset of R^1 : u in U } ; :: thesis: x in [#] R^1

then consider v being set such that

A9: x in v and

A10: v in V by TARSKI:def 4;

thus x in [#] R^1 by A9, A10; :: thesis: verum

defpred S

( $2 = y & y in U & $1 = Int y );

A11: for x being object st x in V holds

ex y being object st

( y in U & S

proof

consider h being Function of V,U such that
let x be object ; :: thesis: ( x in V implies ex y being object st

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

assume A12: x in V ; :: thesis: ex y being object st

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

consider u being Subset of R^1 such that

A13: x = Int u and

A14: u in U by A12;

take u ; :: thesis: ( u in U & S_{1}[x,u] )

thus u in U by A14; :: thesis: S_{1}[x,u]

thus S_{1}[x,u]
by A13, A14; :: thesis: verum

end;( y in U & S

assume A12: x in V ; :: thesis: ex y being object st

( y in U & S

consider u being Subset of R^1 such that

A13: x = Int u and

A14: u in U by A12;

take u ; :: thesis: ( u in U & S

thus u in U by A14; :: thesis: S

thus S

A15: for x being object st x in V holds

S

A16: for x being Element of V

for hx being Subset of R^1 st hx = h . x holds

x = Int hx

proof

reconsider T = R^1 | W as SubSpace of R^1 ;
let x be Element of V; :: thesis: for hx being Subset of R^1 st hx = h . x holds

x = Int hx

let hx be Subset of R^1; :: thesis: ( hx = h . x implies x = Int hx )

assume A17: hx = h . x ; :: thesis: x = Int hx

consider y being Subset of R^1 such that

A18: h . x = y and

y in U and

A19: x = Int y by A15;

thus x = Int hx by A18, A19, A17; :: thesis: verum

end;x = Int hx

let hx be Subset of R^1; :: thesis: ( hx = h . x implies x = Int hx )

assume A17: hx = h . x ; :: thesis: x = Int hx

consider y being Subset of R^1 such that

A18: h . x = y and

y in U and

A19: x = Int y by A15;

thus x = Int hx by A18, A19, A17; :: thesis: verum

V c= bool ([#] T)

proof

then reconsider V1 = V as non empty Subset-Family of T ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V or x in bool ([#] T) )

assume A20: x in V ; :: thesis: x in bool ([#] T)

reconsider xx = x as set by TARSKI:1;

xx c= W

hence x in bool ([#] T) ; :: thesis: verum

end;assume A20: x in V ; :: thesis: x in bool ([#] T)

reconsider xx = x as set by TARSKI:1;

xx c= W

proof

then
xx c= [#] T
by PRE_TOPC:def 5;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in xx or y in W )

thus ( not y in xx or y in W ) by TARSKI:def 4, A20; :: thesis: verum

end;thus ( not y in xx or y in W ) by TARSKI:def 4, A20; :: thesis: verum

hence x in bool ([#] T) ; :: thesis: verum

A21: V1 is open

proof

A25:
the carrier of T c= union V
let v be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not v in V1 or v is open )

assume A22: v in V1 ; :: thesis: v is open

consider u being Subset of R^1 such that

A23: v = Int u and

u in U by A22;

A24: v in the topology of R^1 by A23, PRE_TOPC:def 2;

v /\ ([#] T) = v

end;assume A22: v in V1 ; :: thesis: v is open

consider u being Subset of R^1 such that

A23: v = Int u and

u in U by A22;

A24: v in the topology of R^1 by A23, PRE_TOPC:def 2;

v /\ ([#] T) = v

proof

hence
v is open
by A24, PRE_TOPC:def 4; :: thesis: verum
thus
v /\ ([#] T) c= v
by XBOOLE_1:17; :: according to XBOOLE_0:def 10 :: thesis: v c= v /\ ([#] T)

thus v c= v /\ ([#] T) by XBOOLE_1:19; :: thesis: verum

end;thus v c= v /\ ([#] T) by XBOOLE_1:19; :: thesis: verum

proof

consider B being Subset-Family of T such that
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of T or x in union V )

assume x in the carrier of T ; :: thesis: x in union V

then x in [#] T ;

hence x in union V by PRE_TOPC:def 5; :: thesis: verum

end;assume x in the carrier of T ; :: thesis: x in union V

then x in [#] T ;

hence x in union V by PRE_TOPC:def 5; :: thesis: verum

A26: B c= V and

A27: B is Cover of T and

A28: B is countable by METRIZTS:def 2, A21, A25, SETFAM_1:def 11;

deffunc H

A29: for x being object st x in B holds

H

proof

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

assume x in B ; :: thesis: H_{1}(x) in U

then h . x in rng h by A3, FUNCT_2:4, A26;

hence h . x in U ; :: thesis: verum

end;assume x in B ; :: thesis: H

then h . x in rng h by A3, FUNCT_2:4, A26;

hence h . x in U ; :: thesis: verum

A30: for x being object st x in B holds

f . x = H

reconsider Y = rng f as Subset-Family of Sorgenfrey-line by TOPS_2:2;

A31: Y is Cover of W

proof

A38:
card B c= omega
by CARD_3:def 14, A28;
let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not x in W or x in union Y )

assume A32: x in W ; :: thesis: x in union Y

B is Cover of [#] T by A27;

then B is Cover of W by PRE_TOPC:def 5;

then x in union B by A32, SETFAM_1:def 11, TARSKI:def 3;

then consider b being set such that

A33: ( x in b & b in B ) by TARSKI:def 4;

B = dom f by FUNCT_2:def 1, A3;

then A34: f . b in Y by FUNCT_1:3, A33;

b c= f . b

end;assume A32: x in W ; :: thesis: x in union Y

B is Cover of [#] T by A27;

then B is Cover of W by PRE_TOPC:def 5;

then x in union B by A32, SETFAM_1:def 11, TARSKI:def 3;

then consider b being set such that

A33: ( x in b & b in B ) by TARSKI:def 4;

B = dom f by FUNCT_2:def 1, A3;

then A34: f . b in Y by FUNCT_1:3, A33;

b c= f . b

proof

hence
x in union Y
by A34, TARSKI:def 4, A33; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in b or x in f . b )

assume A35: x in b ; :: thesis: x in f . b

A36: f . b = h . b by A30, A33;

reconsider b1 = b as Element of V by A26, A33;

h . b1 in U by A3;

then reconsider hb = h . b1 as Subset of R^1 by TOPGEN_3:def 2, TOPMETR:17;

A37: b1 = Int hb by A16;

b1 c= hb by A37, TOPS_1:16;

hence x in f . b by A36, A35; :: thesis: verum

end;assume A35: x in b ; :: thesis: x in f . b

A36: f . b = h . b by A30, A33;

reconsider b1 = b as Element of V by A26, A33;

h . b1 in U by A3;

then reconsider hb = h . b1 as Subset of R^1 by TOPGEN_3:def 2, TOPMETR:17;

A37: b1 = Int hb by A16;

b1 c= hb by A37, TOPS_1:16;

hence x in f . b by A36, A35; :: thesis: verum

dom f = B by FUNCT_2:def 1, A3;

then card (rng f) c= card B by CARD_1:12;

then A39: Y is countable by CARD_3:def 14, A38, XBOOLE_1:1;

defpred S

( S = $2 & $1 in S );

A40: for x being object st x in K holds

ex y being object st

( y in U & S

proof

consider g being Function of K,U such that
let x be object ; :: thesis: ( x in K implies ex y being object st

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

assume x in K ; :: thesis: ex y being object st

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

then x in union U by SETFAM_1:def 11, A2, TARSKI:def 3;

then consider Ux being set such that

A41: x in Ux and

A42: Ux in U by TARSKI:def 4;

take Ux ; :: thesis: ( Ux in U & S_{2}[x,Ux] )

thus Ux in U by A42; :: thesis: S_{2}[x,Ux]

thus S_{2}[x,Ux]
by A41; :: thesis: verum

end;( y in U & S

assume x in K ; :: thesis: ex y being object st

( y in U & S

then x in union U by SETFAM_1:def 11, A2, TARSKI:def 3;

then consider Ux being set such that

A41: x in Ux and

A42: Ux in U by TARSKI:def 4;

take Ux ; :: thesis: ( Ux in U & S

thus Ux in U by A42; :: thesis: S

thus S

A43: for x being object st x in K holds

S

set Q = { [.p,r.[ where p, r is Real : r > p } ;

defpred S

( S = $2 & S c= g . $1 & ex x, rx being Real st

( $1 = x & $2 = [.x,rx.[ ) );

A44: for x being object st x in K holds

ex y being object st

( y in { [.p,r.[ where p, r is Real : r > p } & S

proof

consider k being Function of K, { [.p,r.[ where p, r is Real : r > p } such that
let x be object ; :: thesis: ( x in K implies ex y being object st

( y in { [.p,r.[ where p, r is Real : r > p } & S_{3}[x,y] ) )

assume A45: x in K ; :: thesis: ex y being object st

( y in { [.p,r.[ where p, r is Real : r > p } & S_{3}[x,y] )

g . x in U by FUNCT_2:5, A45, A3;

then reconsider gx = g . x as open Subset of Sorgenfrey-line by A1, TOPS_2:def 1;

reconsider x1 = x as Point of Sorgenfrey-line by A45;

S_{2}[x,g . x]
by A43, A45;

then consider a being Subset of Sorgenfrey-line such that

A46: a in BB and

A47: x1 in a and

A48: a c= gx by YELLOW_9:31, Lm8;

consider p, r being Real such that

A49: a = [.p,r.[ and

r > p and

r is rational by Lm7, A46;

reconsider x2 = x1 as Real by A47, A49;

A50: ( p <= x2 & x2 < r ) by A47, A49, XXREAL_1:3;

set y = [.x2,r.[;

take [.x2,r.[ ; :: thesis: ( [.x2,r.[ in { [.p,r.[ where p, r is Real : r > p } & S_{3}[x,[.x2,r.[] )

A51: [.x2,r.[ c= a_{3}[x,[.x2,r.[]

thus S_{3}[x,[.x2,r.[]
by A51, A48, XBOOLE_1:1; :: thesis: verum

end;( y in { [.p,r.[ where p, r is Real : r > p } & S

assume A45: x in K ; :: thesis: ex y being object st

( y in { [.p,r.[ where p, r is Real : r > p } & S

g . x in U by FUNCT_2:5, A45, A3;

then reconsider gx = g . x as open Subset of Sorgenfrey-line by A1, TOPS_2:def 1;

reconsider x1 = x as Point of Sorgenfrey-line by A45;

S

then consider a being Subset of Sorgenfrey-line such that

A46: a in BB and

A47: x1 in a and

A48: a c= gx by YELLOW_9:31, Lm8;

consider p, r being Real such that

A49: a = [.p,r.[ and

r > p and

r is rational by Lm7, A46;

reconsider x2 = x1 as Real by A47, A49;

A50: ( p <= x2 & x2 < r ) by A47, A49, XXREAL_1:3;

set y = [.x2,r.[;

take [.x2,r.[ ; :: thesis: ( [.x2,r.[ in { [.p,r.[ where p, r is Real : r > p } & S

A51: [.x2,r.[ c= a

proof

thus
[.x2,r.[ in { [.p,r.[ where p, r is Real : r > p }
by A50; :: thesis: S
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [.x2,r.[ or z in a )

assume A52: z in [.x2,r.[ ; :: thesis: z in a

reconsider z1 = z as Real by A52;

( x2 <= z1 & z1 < r ) by A52, XXREAL_1:3;

then ( p <= z1 & z1 < r ) by A50, XXREAL_0:2;

hence z in a by A49, XXREAL_1:3; :: thesis: verum

end;assume A52: z in [.x2,r.[ ; :: thesis: z in a

reconsider z1 = z as Real by A52;

( x2 <= z1 & z1 < r ) by A52, XXREAL_1:3;

then ( p <= z1 & z1 < r ) by A50, XXREAL_0:2;

hence z in a by A49, XXREAL_1:3; :: thesis: verum

thus S

A53: for x being object st x in K holds

S

defpred S

( S = $1 & $2 in S );

A54: for x being object st x in rng k holds

ex y being object st

( y in RAT & S

proof

consider j being Function of (rng k),RAT such that
let x be object ; :: thesis: ( x in rng k implies ex y being object st

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

assume A55: x in rng k ; :: thesis: ex y being object st

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

x in { [.p,r.[ where p, r is Real : r > p } by A55;

then consider p, r being Real such that

A56: x = [.p,r.[ and

A57: r > p ;

reconsider xx = x as set by TARSKI:1;

consider y being Rational such that

A58: y in xx by A56, A57, Lm4;

take y ; :: thesis: ( y in RAT & S_{4}[x,y] )

thus y in RAT by RAT_1:def 2; :: thesis: S_{4}[x,y]

take xx ; :: thesis: ( xx = x & y in xx )

thus ( xx = x & y in xx ) by A58; :: thesis: verum

end;( y in RAT & S

assume A55: x in rng k ; :: thesis: ex y being object st

( y in RAT & S

x in { [.p,r.[ where p, r is Real : r > p } by A55;

then consider p, r being Real such that

A56: x = [.p,r.[ and

A57: r > p ;

reconsider xx = x as set by TARSKI:1;

consider y being Rational such that

A58: y in xx by A56, A57, Lm4;

take y ; :: thesis: ( y in RAT & S

thus y in RAT by RAT_1:def 2; :: thesis: S

take xx ; :: thesis: ( xx = x & y in xx )

thus ( xx = x & y in xx ) by A58; :: thesis: verum

A59: for x being object st x in rng k holds

S

A60: for x, y being Element of Sorgenfrey-line st x in K & y in K & x <> y holds

k . x misses k . y

proof

A82:
rng j c= RAT
;
let x, y be Element of Sorgenfrey-line; :: thesis: ( x in K & y in K & x <> y implies k . x misses k . y )

assume that

A61: x in K and

A62: y in K and

A63: x <> y ; :: thesis: k . x misses k . y

A64: ( S_{3}[x,k . x] & S_{3}[y,k . y] )
by A53, A61, A62;

A65: ( g . x in U & g . y in U ) by A3, A61, A62, FUNCT_2:5;

thus (k . x) /\ (k . y) = {} :: according to XBOOLE_0:def 7 :: thesis: verum

end;assume that

A61: x in K and

A62: y in K and

A63: x <> y ; :: thesis: k . x misses k . y

A64: ( S

A65: ( g . x in U & g . y in U ) by A3, A61, A62, FUNCT_2:5;

thus (k . x) /\ (k . y) = {} :: according to XBOOLE_0:def 7 :: thesis: verum

proof

assume
not (k . x) /\ (k . y) = {}
; :: thesis: contradiction

then consider l being object such that

A66: l in (k . x) /\ (k . y) by XBOOLE_0:7;

A67: ( l in k . x & l in k . y ) by XBOOLE_0:def 4, A66;

S_{3}[x,k . x]
by A53, A61;

then consider x1, rx being Real such that

A68: x = x1 and

A69: k . x = [.x1,rx.[ ;

S_{3}[y,k . y]
by A53, A62;

then consider y1, ry being Real such that

A70: y = y1 and

A71: k . y = [.y1,ry.[ ;

reconsider l = l as Real by A69, A66;

A72: ( x1 <= l & l < rx ) by A69, A67, XXREAL_1:3;

A73: ( y1 <= l & l < ry ) by A71, A67, XXREAL_1:3;

end;then consider l being object such that

A66: l in (k . x) /\ (k . y) by XBOOLE_0:7;

A67: ( l in k . x & l in k . y ) by XBOOLE_0:def 4, A66;

S

then consider x1, rx being Real such that

A68: x = x1 and

A69: k . x = [.x1,rx.[ ;

S

then consider y1, ry being Real such that

A70: y = y1 and

A71: k . y = [.y1,ry.[ ;

reconsider l = l as Real by A69, A66;

A72: ( x1 <= l & l < rx ) by A69, A67, XXREAL_1:3;

A73: ( y1 <= l & l < ry ) by A71, A67, XXREAL_1:3;

per cases
( x1 < y1 or x1 > y1 )
by A63, XXREAL_0:1, A68, A70;

end;

suppose A74:
x1 < y1
; :: thesis: contradiction

y1 < rx
by A72, A73, XXREAL_0:2;

then A75: y1 in ].x1,rx.[ by XXREAL_1:4, A74;

reconsider Y = ].x1,rx.[ as Subset of R^1 by TOPMETR:17;

Y c= k . x by XXREAL_1:22, A69;

then A76: Y c= g . x by A64, XBOOLE_1:1;

reconsider gx = g . x as Subset of R^1 by TOPGEN_3:def 2, TOPMETR:17, A65;

A77: y in Int gx by A76, BORSUK_5:40, A70, A75, TOPS_1:22;

Int gx in V by A65;

then y in union V by A77, TARSKI:def 4;

hence contradiction by A62, XBOOLE_0:def 5; :: thesis: verum

end;then A75: y1 in ].x1,rx.[ by XXREAL_1:4, A74;

reconsider Y = ].x1,rx.[ as Subset of R^1 by TOPMETR:17;

Y c= k . x by XXREAL_1:22, A69;

then A76: Y c= g . x by A64, XBOOLE_1:1;

reconsider gx = g . x as Subset of R^1 by TOPGEN_3:def 2, TOPMETR:17, A65;

A77: y in Int gx by A76, BORSUK_5:40, A70, A75, TOPS_1:22;

Int gx in V by A65;

then y in union V by A77, TARSKI:def 4;

hence contradiction by A62, XBOOLE_0:def 5; :: thesis: verum

suppose A78:
x1 > y1
; :: thesis: contradiction

x1 < ry
by A72, A73, XXREAL_0:2;

then A79: x1 in ].y1,ry.[ by XXREAL_1:4, A78;

reconsider X = ].y1,ry.[ as Subset of R^1 by TOPMETR:17;

X c= k . y by XXREAL_1:22, A71;

then A80: X c= g . y by A64, XBOOLE_1:1;

reconsider gy = g . y as Subset of R^1 by A65, TOPGEN_3:def 2, TOPMETR:17;

A81: x in Int gy by A80, BORSUK_5:40, A68, A79, TOPS_1:22;

Int gy in V by A65;

then x in union V by A81, TARSKI:def 4;

hence contradiction by A61, XBOOLE_0:def 5; :: thesis: verum

end;then A79: x1 in ].y1,ry.[ by XXREAL_1:4, A78;

reconsider X = ].y1,ry.[ as Subset of R^1 by TOPMETR:17;

X c= k . y by XXREAL_1:22, A71;

then A80: X c= g . y by A64, XBOOLE_1:1;

reconsider gy = g . y as Subset of R^1 by A65, TOPGEN_3:def 2, TOPMETR:17;

A81: x in Int gy by A80, BORSUK_5:40, A68, A79, TOPS_1:22;

Int gy in V by A65;

then x in union V by A81, TARSKI:def 4;

hence contradiction by A61, XBOOLE_0:def 5; :: thesis: verum

A83: dom j = rng k by FUNCT_2:def 1;

A84: j is one-to-one

proof

A91:
card (rng k) c= omega
by TOPGEN_3:17, CARD_1:10, A82, A83, A84;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom j or not x2 in dom j or not j . x1 = j . x2 or x1 = x2 )

assume that

A85: x1 in dom j and

A86: x2 in dom j and

A87: j . x1 = j . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as set by TARSKI:1;

consider y1 being object such that

A88: ( y1 in dom k & x1 = k . y1 ) by FUNCT_1:def 3, A85;

consider y2 being object such that

A89: ( y2 in dom k & x2 = k . y2 ) by FUNCT_1:def 3, A86;

A90: ( y1 in K & y2 in K ) by A88, A89;

( S_{4}[x1,j . x1] & S_{4}[x2,j . x2] )
by A85, A86, A59;

then (k . y1) /\ (k . y2) <> {} by A88, A89, XBOOLE_0:def 4, A87;

hence x1 = x2 by A88, A89, A60, A90, XBOOLE_0:def 7; :: thesis: verum

end;assume that

A85: x1 in dom j and

A86: x2 in dom j and

A87: j . x1 = j . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as set by TARSKI:1;

consider y1 being object such that

A88: ( y1 in dom k & x1 = k . y1 ) by FUNCT_1:def 3, A85;

consider y2 being object such that

A89: ( y2 in dom k & x2 = k . y2 ) by FUNCT_1:def 3, A86;

A90: ( y1 in K & y2 in K ) by A88, A89;

( S

then (k . y1) /\ (k . y2) <> {} by A88, A89, XBOOLE_0:def 4, A87;

hence x1 = x2 by A88, A89, A60, A90, XBOOLE_0:def 7; :: thesis: verum

A92: [.1,2.[ in { [.p,r.[ where p, r is Real : r > p } ;

then A93: dom k = K by FUNCT_2:def 1;

A94: k is one-to-one

proof

A103:
card K c= card (rng k)
by CARD_1:10, A93, A94;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom k or not x2 in dom k or not k . x1 = k . x2 or x1 = x2 )

assume that

A95: x1 in dom k and

A96: x2 in dom k and

A97: k . x1 = k . x2 ; :: thesis: x1 = x2

A98: ( x1 in K & x2 in K ) by A95, A96;

( k . x1 in rng k & k . x2 in rng k ) by A92, A95, A96, FUNCT_2:4;

then A99: ( k . x1 in { [.p,r.[ where p, r is Real : r > p } & k . x2 in { [.p,r.[ where p, r is Real : r > p } ) ;

consider p1, r1 being Real such that

A100: k . x1 = [.p1,r1.[ and

A101: r1 > p1 by A99;

consider q being Rational such that

A102: q in k . x1 by A100, A101, Lm4;

q in (k . x1) /\ (k . x2) by A102, A97;

hence x1 = x2 by A60, XBOOLE_0:def 7, A98; :: thesis: verum

end;assume that

A95: x1 in dom k and

A96: x2 in dom k and

A97: k . x1 = k . x2 ; :: thesis: x1 = x2

A98: ( x1 in K & x2 in K ) by A95, A96;

( k . x1 in rng k & k . x2 in rng k ) by A92, A95, A96, FUNCT_2:4;

then A99: ( k . x1 in { [.p,r.[ where p, r is Real : r > p } & k . x2 in { [.p,r.[ where p, r is Real : r > p } ) ;

consider p1, r1 being Real such that

A100: k . x1 = [.p1,r1.[ and

A101: r1 > p1 by A99;

consider q being Rational such that

A102: q in k . x1 by A100, A101, Lm4;

q in (k . x1) /\ (k . x2) by A102, A97;

hence x1 = x2 by A60, XBOOLE_0:def 7, A98; :: thesis: verum

A104: card K c= omega by A103, A91, XBOOLE_1:1;

dom g = K by FUNCT_2:def 1, A3;

then card (rng g) c= card K by CARD_1:12;

then A105: rng g is countable by CARD_3:def 14, A104, XBOOLE_1:1;

reconsider Z = rng g as Subset-Family of Sorgenfrey-line by TOPS_2:2;

A106: Z is Cover of K

proof

W c= [#] Sorgenfrey-line
let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not x in K or x in union Z )

assume A107: x in K ; :: thesis: x in union Z

then A108: S_{2}[x,g . x]
by A43;

x in dom g by A107, FUNCT_2:def 1, A3;

then g . x in Z by FUNCT_1:def 3;

hence x in union Z by TARSKI:def 4, A108; :: thesis: verum

end;assume A107: x in K ; :: thesis: x in union Z

then A108: S

x in dom g by A107, FUNCT_2:def 1, A3;

then g . x in Z by FUNCT_1:def 3;

hence x in union Z by TARSKI:def 4, A108; :: thesis: verum

proof

then A109:
W \/ K = [#] Sorgenfrey-line
by XBOOLE_1:45;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in [#] Sorgenfrey-line )

assume x in W ; :: thesis: x in [#] Sorgenfrey-line

then x in [#] R^1 ;

hence x in [#] Sorgenfrey-line by TOPMETR:17, TOPGEN_3:def 2; :: thesis: verum

end;assume x in W ; :: thesis: x in [#] Sorgenfrey-line

then x in [#] R^1 ;

hence x in [#] Sorgenfrey-line by TOPMETR:17, TOPGEN_3:def 2; :: thesis: verum

A110: Z \/ Y is Cover of [#] Sorgenfrey-line

proof

reconsider G = Z \/ Y as Subset-Family of Sorgenfrey-line ;
let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not x in [#] Sorgenfrey-line or x in union (Z \/ Y) )

assume x in [#] Sorgenfrey-line ; :: thesis: x in union (Z \/ Y)

then ( x in W or x in K ) by XBOOLE_0:def 3, A109;

then ( x in union Y or x in union Z ) by A31, A106, TARSKI:def 3, SETFAM_1:def 11;

then x in (union Y) \/ (union Z) by XBOOLE_0:def 3;

hence x in union (Z \/ Y) by ZFMISC_1:78; :: thesis: verum

end;assume x in [#] Sorgenfrey-line ; :: thesis: x in union (Z \/ Y)

then ( x in W or x in K ) by XBOOLE_0:def 3, A109;

then ( x in union Y or x in union Z ) by A31, A106, TARSKI:def 3, SETFAM_1:def 11;

then x in (union Y) \/ (union Z) by XBOOLE_0:def 3;

hence x in union (Z \/ Y) by ZFMISC_1:78; :: thesis: verum

take G ; :: thesis: ( G c= U & G is Cover of the carrier of Sorgenfrey-line & G is countable )

thus G c= U by XBOOLE_1:8; :: thesis: ( G is Cover of the carrier of Sorgenfrey-line & G is countable )

thus G is Cover of Sorgenfrey-line by A110; :: thesis: G is countable

thus G is countable by CARD_2:85, A105, A39; :: thesis: verum