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 ;
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 ;
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 ;
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 ;
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 ;
reconsider xz = xz as Real by A12;
reconsider yz = yz as Real by A12;
A14: ( x <= xz & y <= yz ) by ;
A15: ( - x >= - xz & y <= - xz ) by ;
A16: - x >= y by ;
A17: - x = y by ;
then A18: - x <= yz by ;
A19: - x <= - xz by Lm11, A1, A11, A13, A18;
A20: x >= xz by ;
A21: x = xz by ;
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 ;
A25: |.(x + y).| = - (x + y) by ;
A26: |.(x + y).| > 0 by ;
then x < x + (|.(x + y).| / 2) by ;
then A27: x in Gx by XXREAL_1:3;
y < y + (|.(x + y).| / 2) by ;
then y in Gy by XXREAL_1:3;
then A28: a in G by ;
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 ;
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 ;
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 ;
xz + yz < (x + (|.(x + y).| / 2)) + (y + (|.(x + y).| / 2)) by ;
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;