let A be Subset of Sorgenfrey-plane; :: thesis: ( A = real-anti-diagonal implies Der A is empty )

assume A1: A = real-anti-diagonal ; :: thesis: Der A is empty

assume not Der A is empty ; :: thesis: contradiction

then consider a being object such that

A2: a in Der A by XBOOLE_0:7;

a is_an_accumulation_point_of A by TOPGEN_1:def 3, A2;

then A3: a in Cl (A \ {a}) by TOPGEN_1:def 2;

consider x, y being object such that

A4: ( x in REAL & y in REAL ) and

A5: a = [x,y] by ZFMISC_1:def 2, Lm10, A2;

reconsider x = x, y = y as Real by A4;

assume A1: A = real-anti-diagonal ; :: thesis: Der A is empty

assume not Der A is empty ; :: thesis: contradiction

then consider a being object such that

A2: a in Der A by XBOOLE_0:7;

a is_an_accumulation_point_of A by TOPGEN_1:def 3, A2;

then A3: a in Cl (A \ {a}) by TOPGEN_1:def 2;

consider x, y being object such that

A4: ( x in REAL & y in REAL ) and

A5: a = [x,y] by ZFMISC_1:def 2, Lm10, A2;

reconsider x = x, y = y as Real by A4;

per cases
( y >= - x or y < - x )
;

end;

suppose A6:
y >= - x
; :: thesis: contradiction

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

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

reconsider Gx = [.x,(x + 1).[, Gy = [.y,(y + 1).[ as Subset of Sorgenfrey-line by TOPGEN_3:def 2;

set G = [:Gx,Gy:];

reconsider G = [:Gx,Gy:] as Subset of Sorgenfrey-plane ;

( Gx is open & Gy is open ) by TOPGEN_3:11;

then A7: G is open by BORSUK_1:6;

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

then A8: x in Gx by XXREAL_1:3;

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

then y in Gy by XXREAL_1:3;

then A9: a in G by A5, A8, ZFMISC_1:def 2;

hence contradiction by A7, A9, A3, PRE_TOPC:def 7; :: thesis: verum

end;set Gy = [.y,(y + 1).[;

reconsider Gx = [.x,(x + 1).[, Gy = [.y,(y + 1).[ as Subset of Sorgenfrey-line by TOPGEN_3:def 2;

set G = [:Gx,Gy:];

reconsider G = [:Gx,Gy:] as Subset of Sorgenfrey-plane ;

( Gx is open & Gy is open ) by TOPGEN_3:11;

then A7: G is open by BORSUK_1:6;

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

then A8: x in Gx by XXREAL_1:3;

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

then y in Gy by XXREAL_1:3;

then A9: a in G by A5, A8, ZFMISC_1:def 2;

now :: thesis: not G /\ (A \ {a}) <> {}

then
G misses A \ {a}
by XBOOLE_0:def 7;assume
G /\ (A \ {a}) <> {}
; :: thesis: contradiction

then consider z being object such that

A10: z in G /\ (A \ {a}) by XBOOLE_0:def 1;

( z in G & z in A \ {a} ) by XBOOLE_0:def 4, A10;

then A11: ( z in G & z in A & not z in {a} ) by XBOOLE_0:def 5;

consider xz, yz being object such that

A12: ( xz in [.x,(x + 1).[ & yz in [.y,(y + 1).[ ) and

A13: z = [xz,yz] by ZFMISC_1:def 2, A11;

reconsider xz = xz as Real by A12;

reconsider yz = yz as Real by A12;

A14: ( x <= xz & y <= yz ) by A12, XXREAL_1:3;

A15: ( - x >= - xz & y <= - xz ) by A14, Lm11, A1, A11, A13, XREAL_1:24;

A16: - x >= y by XXREAL_0:2, A15;

A17: - x = y by A16, A6, XXREAL_0:1;

then A18: - x <= yz by A12, XXREAL_1:3;

A19: - x <= - xz by Lm11, A1, A11, A13, A18;

A20: x >= xz by XREAL_1:24, A19;

A21: x = xz by A20, A14, XXREAL_0:1;

then y = yz by A17, Lm11, A1, A11, A13;

hence contradiction by A11, TARSKI:def 1, A13, A5, A21; :: thesis: verum

end;then consider z being object such that

A10: z in G /\ (A \ {a}) by XBOOLE_0:def 1;

( z in G & z in A \ {a} ) by XBOOLE_0:def 4, A10;

then A11: ( z in G & z in A & not z in {a} ) by XBOOLE_0:def 5;

consider xz, yz being object such that

A12: ( xz in [.x,(x + 1).[ & yz in [.y,(y + 1).[ ) and

A13: z = [xz,yz] by ZFMISC_1:def 2, A11;

reconsider xz = xz as Real by A12;

reconsider yz = yz as Real by A12;

A14: ( x <= xz & y <= yz ) by A12, XXREAL_1:3;

A15: ( - x >= - xz & y <= - xz ) by A14, Lm11, A1, A11, A13, XREAL_1:24;

A16: - x >= y by XXREAL_0:2, A15;

A17: - x = y by A16, A6, XXREAL_0:1;

then A18: - x <= yz by A12, XXREAL_1:3;

A19: - x <= - xz by Lm11, A1, A11, A13, A18;

A20: x >= xz by XREAL_1:24, A19;

A21: x = xz by A20, A14, XXREAL_0:1;

then y = yz by A17, Lm11, A1, A11, A13;

hence contradiction by A11, TARSKI:def 1, A13, A5, A21; :: thesis: verum

hence contradiction by A7, A9, A3, PRE_TOPC:def 7; :: thesis: verum

suppose A22:
y < - x
; :: thesis: contradiction

set Gx = [.x,(x + (|.(x + y).| / 2)).[;

set Gy = [.y,(y + (|.(x + y).| / 2)).[;

reconsider Gx = [.x,(x + (|.(x + y).| / 2)).[, Gy = [.y,(y + (|.(x + y).| / 2)).[ as Subset of Sorgenfrey-line by TOPGEN_3:def 2;

reconsider G = [:Gx,Gy:] as Subset of Sorgenfrey-plane ;

( Gx is open & Gy is open ) by TOPGEN_3:11;

then A23: G is open by BORSUK_1:6;

A24: y + x < 0 by A22, XREAL_1:61;

A25: |.(x + y).| = - (x + y) by ABSVALUE:def 1, A22, XREAL_1:61;

A26: |.(x + y).| > 0 by A24, A25, XREAL_1:58;

then x < x + (|.(x + y).| / 2) by XREAL_1:29, XREAL_1:139;

then A27: x in Gx by XXREAL_1:3;

y < y + (|.(x + y).| / 2) by XREAL_1:29, A26, XREAL_1:139;

then y in Gy by XXREAL_1:3;

then A28: a in G by A5, A27, ZFMISC_1:def 2;

hence contradiction by A23, A28, A3, PRE_TOPC:def 7; :: thesis: verum

end;set Gy = [.y,(y + (|.(x + y).| / 2)).[;

reconsider Gx = [.x,(x + (|.(x + y).| / 2)).[, Gy = [.y,(y + (|.(x + y).| / 2)).[ as Subset of Sorgenfrey-line by TOPGEN_3:def 2;

reconsider G = [:Gx,Gy:] as Subset of Sorgenfrey-plane ;

( Gx is open & Gy is open ) by TOPGEN_3:11;

then A23: G is open by BORSUK_1:6;

A24: y + x < 0 by A22, XREAL_1:61;

A25: |.(x + y).| = - (x + y) by ABSVALUE:def 1, A22, XREAL_1:61;

A26: |.(x + y).| > 0 by A24, A25, XREAL_1:58;

then x < x + (|.(x + y).| / 2) by XREAL_1:29, XREAL_1:139;

then A27: x in Gx by XXREAL_1:3;

y < y + (|.(x + y).| / 2) by XREAL_1:29, A26, XREAL_1:139;

then y in Gy by XXREAL_1:3;

then A28: a in G by A5, A27, ZFMISC_1:def 2;

now :: thesis: not G /\ (A \ {a}) <> {}

then
G misses A \ {a}
by XBOOLE_0:def 7;assume
G /\ (A \ {a}) <> {}
; :: thesis: contradiction

then consider z being object such that

A29: z in G /\ (A \ {a}) by XBOOLE_0:def 1;

( z in G & z in A \ {a} ) by A29, XBOOLE_0:def 4;

then A30: ( z in G & z in A & not z in {a} ) by XBOOLE_0:def 5;

consider xz, yz being object such that

A31: ( xz in [.x,(x + (|.(x + y).| / 2)).[ & yz in [.y,(y + (|.(x + y).| / 2)).[ ) and

A32: z = [xz,yz] by ZFMISC_1:def 2, A30;

reconsider xz = xz, yz = yz as Real by A31;

A33: yz = - xz by Lm11, A1, A30, A32;

A34: ( xz < x + (|.(x + y).| / 2) & yz < y + (|.(x + y).| / 2) ) by A31, XXREAL_1:3;

xz + yz < (x + (|.(x + y).| / 2)) + (y + (|.(x + y).| / 2)) by A34, XREAL_1:8;

hence contradiction by A33, A25; :: thesis: verum

end;then consider z being object such that

A29: z in G /\ (A \ {a}) by XBOOLE_0:def 1;

( z in G & z in A \ {a} ) by A29, XBOOLE_0:def 4;

then A30: ( z in G & z in A & not z in {a} ) by XBOOLE_0:def 5;

consider xz, yz being object such that

A31: ( xz in [.x,(x + (|.(x + y).| / 2)).[ & yz in [.y,(y + (|.(x + y).| / 2)).[ ) and

A32: z = [xz,yz] by ZFMISC_1:def 2, A30;

reconsider xz = xz, yz = yz as Real by A31;

A33: yz = - xz by Lm11, A1, A30, A32;

A34: ( xz < x + (|.(x + y).| / 2) & yz < y + (|.(x + y).| / 2) ) by A31, XXREAL_1:3;

xz + yz < (x + (|.(x + y).| / 2)) + (y + (|.(x + y).| / 2)) by A34, XREAL_1:8;

hence contradiction by A33, A25; :: thesis: verum

hence contradiction by A23, A28, A3, PRE_TOPC:def 7; :: thesis: verum