set L = real-anti-diagonal ;
set S2 = Sorgenfrey-plane ;
A1: real-anti-diagonal c= [#] Sorgenfrey-plane

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in real-anti-diagonal or z in [#] Sorgenfrey-plane )
assume z in real-anti-diagonal ; :: thesis: z in [#] Sorgenfrey-plane
then consider x, y being Real such that
A2: z = [x,y] and
y = - x ;
( x in REAL & y in REAL ) by XREAL_0:def 1;
then ( x in [#] Sorgenfrey-line & y in [#] Sorgenfrey-line ) by TOPGEN_3:def 2;
then [x,y] in [:([#] Sorgenfrey-line),([#] Sorgenfrey-line):] by ZFMISC_1:def 2;
hence z in [#] Sorgenfrey-plane by A2; :: thesis: verum

end;

reconsider L = real-anti-diagonal as Subset of Sorgenfrey-plane by A1;
defpred S₁[ 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 & S₁[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 & S₁[z,u] ) )
assume z in the carrier of Sorgenfrey-plane ; :: thesis: ex u being object st
( u in the carrier of R^1 & S₁[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 A4, TOPGEN_3:def 2;
reconsider y = y as Element of REAL by A5, TOPGEN_3:def 2;
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 & S₁[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
S₁[z,f . z] from FUNCT_2:sch 1(A3);
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 A10, XTUPLE_0:1;
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 A11, TOPGEN_3:def 2;
reconsider y = y as Element of REAL by A12, TOPGEN_3:def 2;
A14: f . p = x + y by A13, A8;
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: z in [#] Sorgenfrey-plane
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 A16, TOPGEN_3:def 2;
( u in [#] Sorgenfrey-line & v in [#] Sorgenfrey-line ) ;
then z in [:([#] Sorgenfrey-line),([#] Sorgenfrey-line):] by A17, ZFMISC_1:def 2;
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 A13, ZFMISC_1:def 2;
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 A20, ZFMISC_1:def 2;
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 A22, XXREAL_1:3;
A25: x + y <= x1 + y1 by XREAL_1:7, A24;
(x + y) - r < x + y by XREAL_1:44, XXREAL_0:def 6;
then A26: (x + y) - r < x1 + y1 by A25, XXREAL_0:2;
x1 + y1 < (x + (r / 2)) + (y + (r / 2)) by XREAL_1:8, A24;
then x1 + y1 in ].((f . p) - r),((f . p) + r).[ by A26, A14, XXREAL_1:4;
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 A19, A18; :: 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 TARSKI:def 1, A31;
hence z in f " k by FUNCT_2:38, A29; :: 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 A33, ZFMISC_1:def 2;
reconsider x1 = x as Element of REAL by A34, TOPGEN_3:def 2;
reconsider y1 = y as Element of REAL by A35, TOPGEN_3:def 2;
f . z = x1 + y1 by A8, A36, A32;
then x1 + y1 = 0 by A32, TARSKI:def 1;
then - x1 = y1 ;
hence z in L by A36; :: thesis: verum

end;

hence real-anti-diagonal is closed Subset of Sorgenfrey-plane by A28, A27, TREAL_1:1; :: thesis: verum