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
proof
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
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: v c= 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;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in v or p in U2 /\ L )
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;
hence v is open by A6, A7, PRE_TOPC:def 4; :: thesis: verum
end;
set V = { {v} where v is Element of Sorgenfrey-plane : v in L } ;
{ {v} where v is Element of Sorgenfrey-plane : v in L } c= bool ([#] T)
proof
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
proof
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;
hence z in bool ([#] T) ; :: thesis: verum
end;
then reconsider V = { {v} where v is Element of Sorgenfrey-plane : v in L } as Subset-Family of T ;
A19: V is open
proof
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;
A22: V is Cover of T
proof
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;
defpred S1[ 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 & S1[r,v] )
proof
let r be object ; :: thesis: ( r in REAL implies ex v being object st
( v in V & S1[r,v] ) )
assume r in REAL ; :: thesis: ex v being object st
( v in V & S1[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 & S1[r,v] ) ; :: thesis: verum
end;
consider g being Function of REAL,V such that
A25: for r being object st r in REAL holds
S1[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
proof
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;
rng g c= V ;
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
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 ;
per cases ( G c< V or G = V ) by A39, XBOOLE_0:def 8;
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;
end;
end;
thus not Sorgenfrey-plane is Lindelof by Th4, METRIZTS:def 2, A19, A22, A38; :: thesis: verum