set S2 = Sorgenfrey-plane ;

reconsider L = real-anti-diagonal as Subset of Sorgenfrey-plane by Lm10;

reconsider T = Sorgenfrey-plane | L as SubSpace of Sorgenfrey-plane ;

A1: for v being Subset of T

for z being set st v = {z} & z in L holds

v is open

{ {v} where v is Element of Sorgenfrey-plane : v in L } c= bool ([#] T)

A19: V is open_{1}[ object , object ] means ex x, y being Real st

( $1 = x & $2 = {[x,y]} );

A23: for r being object st r in REAL holds

ex v being object st

( v in V & S_{1}[r,v] )

A25: for r being object st r in REAL holds

S_{1}[r,g . r]
from FUNCT_2:sch 1(A23);

reconsider x = 1 as Element of REAL by XREAL_0:def 1;

reconsider y = - 1 as Element of REAL by XREAL_0:def 1;

set z = [x,y];

A26: [x,y] in L ;

then reconsider z = [x,y] as Element of Sorgenfrey-plane ;

{z} in V by A26;

then A27: dom g = REAL by FUNCT_2:def 1;

A28: g is one-to-one

then A36: card REAL c= card V by CARD_1:10, A28, A27;

A37: not card V c= omega by A36, TOPGEN_3:30, TOPGEN_3:def 4;

A38: for G being Subset-Family of T holds

( not G c= V or not G is Cover of T or not G is countable )

reconsider L = real-anti-diagonal as Subset of Sorgenfrey-plane by Lm10;

reconsider T = Sorgenfrey-plane | L as SubSpace of Sorgenfrey-plane ;

A1: for v being Subset of T

for z being set st v = {z} & z in L holds

v is open

proof

set V = { {v} where v is Element of Sorgenfrey-plane : v in L } ;
let v be Subset of T; :: thesis: for z being set st v = {z} & z in L holds

v is open

let z be set ; :: thesis: ( v = {z} & z in L implies v is open )

assume that

A2: v = {z} and

A3: z in L ; :: thesis: v is open

consider x, y being Real such that

A4: z = [x,y] and

A5: y = - x by A3;

set Ux = [.x,(x + 1).[;

reconsider Ux = [.x,(x + 1).[ as open Subset of Sorgenfrey-line by TOPGEN_3:11;

set Uy = [.y,(y + 1).[;

reconsider Uy = [.y,(y + 1).[ as open Subset of Sorgenfrey-line by TOPGEN_3:11;

reconsider U2 = [:Ux,Uy:] as Subset of Sorgenfrey-plane ;

A6: U2 in the topology of Sorgenfrey-plane by BORSUK_1:6, PRE_TOPC:def 2;

A7: U2 /\ L = v

hence v is open by A6, A7, PRE_TOPC:def 4; :: thesis: verum

end;v is open

let z be set ; :: thesis: ( v = {z} & z in L implies v is open )

assume that

A2: v = {z} and

A3: z in L ; :: thesis: v is open

consider x, y being Real such that

A4: z = [x,y] and

A5: y = - x by A3;

set Ux = [.x,(x + 1).[;

reconsider Ux = [.x,(x + 1).[ as open Subset of Sorgenfrey-line by TOPGEN_3:11;

set Uy = [.y,(y + 1).[;

reconsider Uy = [.y,(y + 1).[ as open Subset of Sorgenfrey-line by TOPGEN_3:11;

reconsider U2 = [:Ux,Uy:] as Subset of Sorgenfrey-plane ;

A6: U2 in the topology of Sorgenfrey-plane by BORSUK_1:6, PRE_TOPC:def 2;

A7: U2 /\ L = v

proof

assume p in v ; :: thesis: p in U2 /\ L

then A15: p = z by A2, TARSKI:def 1;

( x < x + 1 & y < y + 1 ) by XREAL_1:29;

then ( x in Ux & y in Uy ) by XXREAL_1:3;

then p in U2 by ZFMISC_1:def 2, A15, A4;

hence p in U2 /\ L by XBOOLE_0:def 4, A15, A3; :: thesis: verum

end;

L = [#] T
by PRE_TOPC:def 5;hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: v c= U2 /\ L

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in v or p in U2 /\ L )let p be object ; :: thesis: ( p in U2 /\ L implies p in v )

assume p in U2 /\ L ; :: thesis: p in v

then A8: ( p in U2 & p in L ) by XBOOLE_0:def 4;

then consider p1, p2 being object such that

A9: ( p1 in Ux & p2 in Uy ) and

A10: p = [p1,p2] by ZFMISC_1:def 2;

consider r1, r2 being Real such that

A11: p = [r1,r2] and

A12: r2 = - r1 by A8;

( p1 = r1 & p2 = r2 ) by XTUPLE_0:1, A10, A11;

then A13: ( r1 >= x & r1 < x + 1 & r2 >= y & r2 < y + 1 ) by XXREAL_1:3, A9;

then r1 <= x by XREAL_1:24, A5, A12;

then A14: r1 = x by A13, XXREAL_0:1;

r2 <= y by XREAL_1:24, A12, A13, A5;

then r2 = y by A13, XXREAL_0:1;

hence p in v by A2, A14, A11, A4, TARSKI:def 1; :: thesis: verum

end;assume p in U2 /\ L ; :: thesis: p in v

then A8: ( p in U2 & p in L ) by XBOOLE_0:def 4;

then consider p1, p2 being object such that

A9: ( p1 in Ux & p2 in Uy ) and

A10: p = [p1,p2] by ZFMISC_1:def 2;

consider r1, r2 being Real such that

A11: p = [r1,r2] and

A12: r2 = - r1 by A8;

( p1 = r1 & p2 = r2 ) by XTUPLE_0:1, A10, A11;

then A13: ( r1 >= x & r1 < x + 1 & r2 >= y & r2 < y + 1 ) by XXREAL_1:3, A9;

then r1 <= x by XREAL_1:24, A5, A12;

then A14: r1 = x by A13, XXREAL_0:1;

r2 <= y by XREAL_1:24, A12, A13, A5;

then r2 = y by A13, XXREAL_0:1;

hence p in v by A2, A14, A11, A4, TARSKI:def 1; :: thesis: verum

assume p in v ; :: thesis: p in U2 /\ L

then A15: p = z by A2, TARSKI:def 1;

( x < x + 1 & y < y + 1 ) by XREAL_1:29;

then ( x in Ux & y in Uy ) by XXREAL_1:3;

then p in U2 by ZFMISC_1:def 2, A15, A4;

hence p in U2 /\ L by XBOOLE_0:def 4, A15, A3; :: thesis: verum

hence v is open by A6, A7, PRE_TOPC:def 4; :: thesis: verum

{ {v} where v is Element of Sorgenfrey-plane : v in L } c= bool ([#] T)

proof

then reconsider V = { {v} where v is Element of Sorgenfrey-plane : v in L } as Subset-Family of T ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { {v} where v is Element of Sorgenfrey-plane : v in L } or z in bool ([#] T) )

reconsider zz = z as set by TARSKI:1;

assume z in { {v} where v is Element of Sorgenfrey-plane : v in L } ; :: thesis: z in bool ([#] T)

then consider v being Element of Sorgenfrey-plane such that

A16: z = {v} and

A17: v in L ;

A18: v in [#] T by A17, PRE_TOPC:def 5;

zz c= [#] T

end;reconsider zz = z as set by TARSKI:1;

assume z in { {v} where v is Element of Sorgenfrey-plane : v in L } ; :: thesis: z in bool ([#] T)

then consider v being Element of Sorgenfrey-plane such that

A16: z = {v} and

A17: v in L ;

A18: v in [#] T by A17, PRE_TOPC:def 5;

zz c= [#] T

proof

hence
z in bool ([#] T)
; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in zz or y in [#] T )

assume y in zz ; :: thesis: y in [#] T

hence y in [#] T by TARSKI:def 1, A16, A18; :: thesis: verum

end;assume y in zz ; :: thesis: y in [#] T

hence y in [#] T by TARSKI:def 1, A16, A18; :: thesis: verum

A19: V is open

proof

A22:
V is Cover of T
let u be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not u in V or u is open )

assume u in V ; :: thesis: u is open

then consider z being Element of Sorgenfrey-plane such that

A20: u = {z} and

A21: z in L ;

thus u is open by A20, A21, A1; :: thesis: verum

end;assume u in V ; :: thesis: u is open

then consider z being Element of Sorgenfrey-plane such that

A20: u = {z} and

A21: z in L ;

thus u is open by A20, A21, A1; :: thesis: verum

proof

defpred S
let z be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not z in the carrier of T or z in union V )

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

then z in [#] T ;

then z in L by PRE_TOPC:def 5;

then ( {z} in V & z in {z} ) by TARSKI:def 1;

hence z in union V by TARSKI:def 4; :: thesis: verum

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

then z in [#] T ;

then z in L by PRE_TOPC:def 5;

then ( {z} in V & z in {z} ) by TARSKI:def 1;

hence z in union V by TARSKI:def 4; :: thesis: verum

( $1 = x & $2 = {[x,y]} );

A23: for r being object st r in REAL holds

ex v being object st

( v in V & S

proof

consider g being Function of REAL,V such that
let r be object ; :: thesis: ( r in REAL implies ex v being object st

( v in V & S_{1}[r,v] ) )

assume r in REAL ; :: thesis: ex v being object st

( v in V & S_{1}[r,v] )

then reconsider r = r as Real ;

reconsider y = - r as Real ;

set u = [r,y];

A24: [r,y] in L ;

then reconsider u = [r,y] as Element of Sorgenfrey-plane ;

set v = {u};

{u} in V by A24;

hence ex v being object st

( v in V & S_{1}[r,v] )
; :: thesis: verum

end;( v in V & S

assume r in REAL ; :: thesis: ex v being object st

( v in V & S

then reconsider r = r as Real ;

reconsider y = - r as Real ;

set u = [r,y];

A24: [r,y] in L ;

then reconsider u = [r,y] as Element of Sorgenfrey-plane ;

set v = {u};

{u} in V by A24;

hence ex v being object st

( v in V & S

A25: for r being object st r in REAL holds

S

reconsider x = 1 as Element of REAL by XREAL_0:def 1;

reconsider y = - 1 as Element of REAL by XREAL_0:def 1;

set z = [x,y];

A26: [x,y] in L ;

then reconsider z = [x,y] as Element of Sorgenfrey-plane ;

{z} in V by A26;

then A27: dom g = REAL by FUNCT_2:def 1;

A28: g is one-to-one

proof

rng g c= V
;
let r1, r2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not r1 in dom g or not r2 in dom g or not g . r1 = g . r2 or r1 = r2 )

assume that

A29: r1 in dom g and

A30: r2 in dom g and

A31: g . r1 = g . r2 ; :: thesis: r1 = r2

consider x1, y1 being Real such that

A32: r1 = x1 and

A33: g . r1 = {[x1,y1]} by A25, A29;

consider x2, y2 being Real such that

A34: r2 = x2 and

A35: g . r2 = {[x2,y2]} by A25, A30;

[x1,y1] = [x2,y2] by ZFMISC_1:3, A35, A33, A31;

hence r1 = r2 by A32, A34, XTUPLE_0:1; :: thesis: verum

end;assume that

A29: r1 in dom g and

A30: r2 in dom g and

A31: g . r1 = g . r2 ; :: thesis: r1 = r2

consider x1, y1 being Real such that

A32: r1 = x1 and

A33: g . r1 = {[x1,y1]} by A25, A29;

consider x2, y2 being Real such that

A34: r2 = x2 and

A35: g . r2 = {[x2,y2]} by A25, A30;

[x1,y1] = [x2,y2] by ZFMISC_1:3, A35, A33, A31;

hence r1 = r2 by A32, A34, XTUPLE_0:1; :: thesis: verum

then A36: card REAL c= card V by CARD_1:10, A28, A27;

A37: not card V c= omega by A36, TOPGEN_3:30, TOPGEN_3:def 4;

A38: for G being Subset-Family of T holds

( not G c= V or not G is Cover of T or not G is countable )

proof

thus
not Sorgenfrey-plane is Lindelof
by Th4, METRIZTS:def 2, A19, A22, A38; :: thesis: verum
assume
ex G being Subset-Family of T st

( G c= V & G is Cover of T & G is countable ) ; :: thesis: contradiction

then consider G being Subset-Family of T such that

A39: G c= V and

A40: G is Cover of T and

A41: G is countable ;

end;( G c= V & G is Cover of T & G is countable ) ; :: thesis: contradiction

then consider G being Subset-Family of T such that

A39: G c= V and

A40: G is Cover of T and

A41: G is countable ;

per cases
( G c< V or G = V )
by A39, XBOOLE_0:def 8;

end;

suppose
G c< V
; :: thesis: contradiction

then consider u being object such that

A42: u in V and

A43: not u in G by XBOOLE_0:6;

consider v being Element of Sorgenfrey-plane such that

A44: u = {v} and

A45: v in L by A42;

A46: [#] T c= union G by SETFAM_1:def 11, A40;

v in [#] T by A45, PRE_TOPC:def 5;

then consider u1 being set such that

A47: v in u1 and

A48: u1 in G by TARSKI:def 4, A46;

u1 in V by A39, A48;

then consider v1 being Element of Sorgenfrey-plane such that

A49: u1 = {v1} and

v1 in L ;

thus contradiction by A43, A44, A49, A48, A47, TARSKI:def 1; :: thesis: verum

end;A42: u in V and

A43: not u in G by XBOOLE_0:6;

consider v being Element of Sorgenfrey-plane such that

A44: u = {v} and

A45: v in L by A42;

A46: [#] T c= union G by SETFAM_1:def 11, A40;

v in [#] T by A45, PRE_TOPC:def 5;

then consider u1 being set such that

A47: v in u1 and

A48: u1 in G by TARSKI:def 4, A46;

u1 in V by A39, A48;

then consider v1 being Element of Sorgenfrey-plane such that

A49: u1 = {v1} and

v1 in L ;

thus contradiction by A43, A44, A49, A48, A47, TARSKI:def 1; :: thesis: verum