set L = real-anti-diagonal ;
set S2 = Sorgenfrey-plane ;
A1: real-anti-diagonal c= [#] Sorgenfrey-plane
proof end;
reconsider L = real-anti-diagonal as Subset of Sorgenfrey-plane by A1;
defpred S1[ object , object ] means ex x, y being Real st
( \$1 = [x,y] & \$2 = x + y );
A3: for z being object st z in the carrier of Sorgenfrey-plane holds
ex u being object st
( u in the carrier of R^1 & S1[z,u] )
proof
let z be object ; :: thesis: ( z in the carrier of Sorgenfrey-plane implies ex u being object st
( u in the carrier of R^1 & S1[z,u] ) )

assume z in the carrier of Sorgenfrey-plane ; :: thesis: ex u being object st
( u in the carrier of R^1 & S1[z,u] )

then z in [: the carrier of Sorgenfrey-line, the carrier of Sorgenfrey-line:] by BORSUK_1:def 2;
then consider x, y being object such that
A4: x in the carrier of Sorgenfrey-line and
A5: y in the carrier of Sorgenfrey-line and
A6: z = [x,y] by ZFMISC_1:def 2;
reconsider x = x as Element of REAL by ;
reconsider y = y as Element of REAL by ;
set u = x + y;
x + y in the carrier of R^1 by TOPMETR:17;
hence ex u being object st
( u in the carrier of R^1 & S1[z,u] ) by A6; :: thesis: verum
end;
consider f being Function of Sorgenfrey-plane,R^1 such that
A7: for z being object st z in the carrier of Sorgenfrey-plane holds
S1[z,f . z] from A8: for x, y being Element of REAL st [x,y] in the carrier of Sorgenfrey-plane holds
f . [x,y] = x + y
proof
let x, y be Element of REAL ; :: thesis: ( [x,y] in the carrier of Sorgenfrey-plane implies f . [x,y] = x + y )
assume A9: [x,y] in the carrier of Sorgenfrey-plane ; :: thesis: f . [x,y] = x + y
consider x1, y1 being Real such that
A10: ( [x,y] = [x1,y1] & f . [x,y] = x1 + y1 ) by A9, A7;
( x = x1 & y = y1 ) by ;
hence f . [x,y] = x + y by A10; :: thesis: verum
end;
for p being Point of Sorgenfrey-plane
for r being positive Real ex W being open Subset of Sorgenfrey-plane st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )
proof
let p be Point of Sorgenfrey-plane; :: thesis: for r being positive Real ex W being open Subset of Sorgenfrey-plane st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )

let r be positive Real; :: thesis: ex W being open Subset of Sorgenfrey-plane st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )

p in [#] Sorgenfrey-plane ;
then p in [: the carrier of Sorgenfrey-line, the carrier of Sorgenfrey-line:] by BORSUK_1:def 2;
then consider x, y being object such that
A11: x in the carrier of Sorgenfrey-line and
A12: y in the carrier of Sorgenfrey-line and
A13: p = [x,y] by ZFMISC_1:def 2;
reconsider x = x as Element of REAL by ;
reconsider y = y as Element of REAL by ;
A14: f . p = x + y by ;
set U = ].((f . p) - r),((f . p) + r).[;
set W = [:[.x,(x + (r / 2)).[,[.y,(y + (r / 2)).[:];
A15: [:[.x,(x + (r / 2)).[,[.y,(y + (r / 2)).[:] c= [#] Sorgenfrey-plane
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:[.x,(x + (r / 2)).[,[.y,(y + (r / 2)).[:] or z in [#] Sorgenfrey-plane )
assume z in [:[.x,(x + (r / 2)).[,[.y,(y + (r / 2)).[:] ; :: thesis:
then consider u, v being object such that
A16: ( u in [.x,(x + (r / 2)).[ & v in [.y,(y + (r / 2)).[ ) and
A17: z = [u,v] by ZFMISC_1:def 2;
reconsider u = u, v = v as Element of [#] Sorgenfrey-line by ;
( u in [#] Sorgenfrey-line & v in [#] Sorgenfrey-line ) ;
then z in by ;
hence z in [#] Sorgenfrey-plane ; :: thesis: verum
end;
reconsider W = [:[.x,(x + (r / 2)).[,[.y,(y + (r / 2)).[:] as Subset of Sorgenfrey-plane by A15;
reconsider X = [.x,(x + (r / 2)).[ as Subset of Sorgenfrey-line by TOPGEN_3:def 2;
reconsider Y = [.y,(y + (r / 2)).[ as Subset of Sorgenfrey-line by TOPGEN_3:def 2;
( X is open & Y is open ) by TOPGEN_3:11;
then A18: W is open by BORSUK_1:6;
r / 2 is positive ;
then ( x < x + (r / 2) & y < y + (r / 2) ) by XREAL_1:29;
then ( x in [.x,(x + (r / 2)).[ & y in [.y,(y + (r / 2)).[ ) by XXREAL_1:3;
then A19: p in W by ;
f .: W c= ].((f . p) - r),((f . p) + r).[
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f .: W or z in ].((f . p) - r),((f . p) + r).[ )
assume z in f .: W ; :: thesis: z in ].((f . p) - r),((f . p) + r).[
then consider w being object such that
w in dom f and
A20: w in W and
A21: z = f . w by FUNCT_1:def 6;
consider x1, y1 being object such that
A22: ( x1 in X & y1 in Y ) and
A23: w = [x1,y1] by ;
reconsider x1 = x1 as Element of REAL by A22;
reconsider y1 = y1 as Element of REAL by A22;
A24: ( x <= x1 & x1 < x + (r / 2) & y <= y1 & y1 < y + (r / 2) ) by ;
A25: x + y <= x1 + y1 by ;
(x + y) - r < x + y by ;
then A26: (x + y) - r < x1 + y1 by ;
x1 + y1 < (x + (r / 2)) + (y + (r / 2)) by ;
then x1 + y1 in ].((f . p) - r),((f . p) + r).[ by ;
hence z in ].((f . p) - r),((f . p) + r).[ by A23, A8, A20, A21; :: thesis: verum
end;
hence ex W being open Subset of Sorgenfrey-plane st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by ; :: thesis: verum
end;
then A27: f is continuous by TOPS_4:21;
reconsider zz = 0 as Element of REAL by XREAL_0:def 1;
reconsider k = {zz} as Subset of R^1 by TOPMETR:17;
reconsider k1 = [.zz,zz.] as Subset of R^1 by TOPMETR:17;
A28: k = k1 by XXREAL_1:17;
L = f " k
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: f " k c= L
let z be object ; :: thesis: ( z in L implies z in f " k )
assume A29: z in L ; :: thesis: z in f " k
then consider x, y being Real such that
A30: z = [x,y] and
A31: y = - x ;
reconsider x = x, y = y as Element of REAL by XREAL_0:def 1;
f . z = x + y by A8, A30, A29;
then f . z in k by ;
hence z in f " k by ; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f " k or z in L )
assume z in f " k ; :: thesis: z in L
then A32: ( z in [#] Sorgenfrey-plane & f . z in k ) by FUNCT_2:38;
then A33: z in [: the carrier of Sorgenfrey-line, the carrier of Sorgenfrey-line:] by BORSUK_1:def 2;
consider x, y being object such that
A34: x in the carrier of Sorgenfrey-line and
A35: y in the carrier of Sorgenfrey-line and
A36: z = [x,y] by ;
reconsider x1 = x as Element of REAL by ;
reconsider y1 = y as Element of REAL by ;
f . z = x1 + y1 by A8, A36, A32;
then x1 + y1 = 0 by ;
then - x1 = y1 ;
hence z in L by A36; :: thesis: verum
end;
hence real-anti-diagonal is closed Subset of Sorgenfrey-plane by ; :: thesis: verum