set L = real-anti-diagonal ;

set S2 = Sorgenfrey-plane ;

A1: real-anti-diagonal c= [#] Sorgenfrey-plane

defpred S_{1}[ 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_{1}[z,u] )

A7: for z being object st z in the carrier of Sorgenfrey-plane holds

S_{1}[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

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).[ )

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

set S2 = Sorgenfrey-plane ;

A1: real-anti-diagonal c= [#] Sorgenfrey-plane

proof

reconsider L = real-anti-diagonal as Subset of Sorgenfrey-plane by A1;
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;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

defpred S

( $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

proof

consider f being Function of Sorgenfrey-plane,R^1 such that
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_{1}[z,u] ) )

assume z in the carrier of Sorgenfrey-plane ; :: thesis: ex u being object st

( u in the carrier of R^1 & S_{1}[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_{1}[z,u] )
by A6; :: thesis: verum

end;( u in the carrier of R^1 & S

assume z in the carrier of Sorgenfrey-plane ; :: thesis: ex u being object st

( u in the carrier of R^1 & S

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

A7: for z being object st z in the carrier of Sorgenfrey-plane holds

S

A8: for x, y being Element of REAL st [x,y] in the carrier of Sorgenfrey-plane holds

f . [x,y] = x + y

proof

for p being Point of Sorgenfrey-plane
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;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

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

then A27:
f is continuous
by TOPS_4:21;
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

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).[

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A19, A18; :: thesis: verum

end;( 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

reconsider W = [:[.x,(x + (r / 2)).[,[.y,(y + (r / 2)).[:] as Subset of Sorgenfrey-plane by A15;
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;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

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

hence
ex W being open Subset of Sorgenfrey-plane st
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;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

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A19, A18; :: thesis: verum

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

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: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: f " k c= L

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f " k or z in 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;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

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