set S = Sorgenfrey-line ;
let U be Subset-Family of Sorgenfrey-line; :: according to METRIZTS:def 2 :: thesis:
assume that
A1: U is open and
A2: U is Cover of Sorgenfrey-line ; :: thesis:
A3: U <> {}

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

end;

set V = { (Int u) where u is Subset of R^1 : u in 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

proof

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)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in { (Int u) where u is Subset of R^1 : u in U } ; :: thesis:
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:

end;

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

end;

then reconsider V = { (Int u) where u is Subset of R^1 : u in U } as non empty Subset-Family of R^1 ;
union { (Int u) where u is Subset of R^1 : u in U } c= [#] R^1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union { (Int u) where u is Subset of R^1 : u in U } ; :: thesis:
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:

end;

then reconsider W = union { (Int u) where u is Subset of R^1 : u in U } as Subset of R^1 ;
defpred S₁[ 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₁[x,y] )

proof

let x be object ; :: thesis:
assume A12: x in V ; :: thesis:
consider u being Subset of R^1 such that
A13: x = Int u and
A14: u in U by A12;
take u ; :: thesis:
thus u in U by A14; :: thesis:
thus S₁[x,u] by A13, A14; :: thesis:

end;

consider h being Function of V,U such that
A15: for x being object st x in V holds
S₁[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

proof

let x be Element of V; :: thesis:
let hx be Subset of R^1; :: thesis:
assume A17: hx = h . x ; :: thesis:
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:

end;

reconsider T = R^1 | W as SubSpace of R^1 ;
V c= bool ([#] T)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A20: x in V ; :: thesis:
reconsider xx = x as set by TARSKI:1;
xx c= W

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
thus ( not y in xx or y in W ) by TARSKI:def 4, A20; :: thesis:

end;

then xx c= [#] T by PRE_TOPC:def 5;
hence x in bool ([#] T) ; :: thesis:

end;

then reconsider V1 = V as non empty Subset-Family of T ;
A21: V1 is open

proof

let v be Subset of T; :: according to TOPS_2:def 1 :: thesis:
assume A22: v in V1 ; :: thesis:
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

thus v /\ ([#] T) c= v by XBOOLE_1:17; :: according to XBOOLE_0:def 10 :: thesis:
thus v c= v /\ ([#] T) by XBOOLE_1:19; :: thesis:

end;

hence v is open by A24, PRE_TOPC:def 4; :: thesis:

end;

A25: the carrier of T c= union V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier of T ; :: thesis:
then x in [#] T ;
hence x in union V by PRE_TOPC:def 5; :: thesis:

end;

consider B being Subset-Family of T such that
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₁( object ) -> set = h . $1;
A29: for x being object st x in B holds
H₁(x) in U

proof

let x be object ; :: thesis:
assume x in B ; :: thesis:
then h . x in rng h by A3, FUNCT_2:4, A26;
hence h . x in U ; :: thesis:

end;

consider f being Function of B,U such that
A30: for x being object st x in B holds
f . x = H₁(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

proof

let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
assume A32: x in W ; :: thesis:
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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A35: x in b ; :: thesis:
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:

end;

hence x in union Y by A34, TARSKI:def 4, A33; :: thesis:

end;

A38: card B c= omega by CARD_3:def 14, A28;
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₂[ 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₂[x,y] )

proof

let x be object ; :: thesis:
assume x in K ; :: thesis:
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:
thus Ux in U by A42; :: thesis:
thus S₂[x,Ux] by A41; :: thesis:

end;

consider g being Function of K,U such that
A43: for x being object st x in K holds
S₂[x,g . x] from FUNCT_2:sch 1(A40);
set Q = { [.p,r.[ where p, r is Real : r > p } ;
defpred S₃[ 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₃[x,y] )

proof

let x be object ; :: thesis:
assume A45: x in K ; :: thesis:
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₂[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:
A51: [.x2,r.[ c= a

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A52: z in [.x2,r.[ ; :: thesis:
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:

end;

thus [.x2,r.[ in { [.p,r.[ where p, r is Real : r > p } by A50; :: thesis:
thus S₃[x,[.x2,r.[] by A51, A48, XBOOLE_1:1; :: thesis:

end;

consider k being Function of K, { [.p,r.[ where p, r is Real : r > p } such that
A53: for x being object st x in K holds
S₃[x,k . x] from FUNCT_2:sch 1(A44);
defpred S₄[ 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₄[x,y] )

proof

let x be object ; :: thesis:
assume A55: x in rng k ; :: thesis:
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:
thus y in RAT by RAT_1:def 2; :: thesis:
take xx ; :: thesis:
thus ( xx = x & y in xx ) by A58; :: thesis:

end;

consider j being Function of (rng k),RAT such that
A59: for x being object st x in rng k holds
S₄[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

proof

let x, y be Element of Sorgenfrey-line; :: thesis:
assume that
A61: x in K and
A62: y in K and
A63: x <> y ; :: thesis:
A64: ( S₃[x,k . x] & S₃[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:

proof

assume not (k . x) /\ (k . y) = {} ; :: thesis:
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₃[x,k . x] by A53, A61;
then consider x1, rx being Real such that
A68: x = x1 and
A69: k . x = [.x1,rx.[ ;
S₃[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;

per cases by A63, XXREAL_0:1, A68, A70;

suppose A74: x1 < y1 ; :: thesis:

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:

end;

suppose A78: x1 > y1 ; :: thesis:

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:

end;

A82: rng j c= RAT ;
A83: dom j = rng k by FUNCT_2:def 1;
A84: j is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A85: x1 in dom j and
A86: x2 in dom j and
A87: j . x1 = j . x2 ; :: thesis:
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₄[x1,j . x1] & S₄[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:

end;

A91: card (rng k) c= omega by TOPGEN_3:17, CARD_1:10, A82, A83, A84;
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

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A95: x1 in dom k and
A96: x2 in dom k and
A97: k . x1 = k . x2 ; :: thesis:
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:

end;

A103: card K c= card (rng k) by CARD_1:10, A93, A94;
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

let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
assume A107: x in K ; :: thesis:
then A108: S₂[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:

end;

W c= [#] Sorgenfrey-line

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in W ; :: thesis:
then x in [#] R^1 ;
hence x in [#] Sorgenfrey-line by TOPMETR:17, TOPGEN_3:def 2; :: thesis:

end;

then A109: W \/ K = [#] Sorgenfrey-line by XBOOLE_1:45;
A110: Z \/ Y is Cover of [#] Sorgenfrey-line

proof

let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
assume x in [#] Sorgenfrey-line ; :: thesis:
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:

end;

reconsider G = Z \/ Y as Subset-Family of Sorgenfrey-line ;
take G ; :: thesis:
thus G c= U by XBOOLE_1:8; :: thesis:
thus G is Cover of Sorgenfrey-line by A110; :: thesis:
thus G is countable by CARD_2:85, A105, A39; :: thesis: