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;
per cases ( y >= - x or y < - x ) ;
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;
now :: thesis: not G /\ (A \ {a}) <> {}
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 G misses A \ {a} by XBOOLE_0:def 7;
hence contradiction by A7, A9, A3, PRE_TOPC:def 7; :: thesis: verum
end;
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;
now :: thesis: not G /\ (A \ {a}) <> {}
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 G misses A \ {a} by XBOOLE_0:def 7;
hence contradiction by A23, A28, A3, PRE_TOPC:def 7; :: thesis: verum
end;
end;