set T = Sorgenfrey-line ;
consider B being Subset-Family of REAL such that
A1:
the topology of Sorgenfrey-line = UniCl B
and
A2:
B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) }
by TOPGEN_3:def 2;
let x, y be Point of Sorgenfrey-line; URYSOHN1:def 7 ( x = y or ex b1, b2 being Element of bool the carrier of Sorgenfrey-line st
( b1 is open & b2 is open & x in b1 & not y in b1 & y in b2 & not x in b2 ) )
reconsider a = x, b = y as Element of REAL by TOPGEN_3:def 2;
A3:
B c= the topology of Sorgenfrey-line
by A1, CANTOR_1:1;
assume A4:
x <> y
; ex b1, b2 being Element of bool the carrier of Sorgenfrey-line st
( b1 is open & b2 is open & x in b1 & not y in b1 & y in b2 & not x in b2 )
per cases
( a < b or a > b )
by A4, XXREAL_0:1;
suppose A5:
a < b
;
ex b1, b2 being Element of bool the carrier of Sorgenfrey-line st
( b1 is open & b2 is open & x in b1 & not y in b1 & y in b2 & not x in b2 )
b < b + 1
by XREAL_1:29;
then consider q being
Rational such that A6:
b < q
and
q < b + 1
by RAT_1:7;
[.b,q.[ in B
by A2, A6;
then A7:
[.b,q.[ in the
topology of
Sorgenfrey-line
by A3;
consider w being
Rational such that A8:
a < w
and A9:
w < b
by A5, RAT_1:7;
[.a,w.[ in B
by A2, A8;
then
[.a,w.[ in the
topology of
Sorgenfrey-line
by A3;
then reconsider U =
[.a,w.[,
V =
[.b,q.[ as
open Subset of
Sorgenfrey-line by A7, PRE_TOPC:def 2;
take
U
;
ex b1 being Element of bool the carrier of Sorgenfrey-line st
( U is open & b1 is open & x in U & not y in U & y in b1 & not x in b1 )take
V
;
( U is open & V is open & x in U & not y in U & y in V & not x in V )thus
(
U is
open &
V is
open )
;
( x in U & not y in U & y in V & not x in V )thus
(
x in U & not
y in U &
y in V & not
x in V )
by A5, A8, A9, A6, XXREAL_1:3;
verum end; suppose A10:
a > b
;
ex b1, b2 being Element of bool the carrier of Sorgenfrey-line st
( b1 is open & b2 is open & x in b1 & not y in b1 & y in b2 & not x in b2 )
a < a + 1
by XREAL_1:29;
then consider q being
Rational such that A11:
a < q
and
q < a + 1
by RAT_1:7;
[.a,q.[ in B
by A2, A11;
then A12:
[.a,q.[ in the
topology of
Sorgenfrey-line
by A3;
consider w being
Rational such that A13:
b < w
and A14:
w < a
by A10, RAT_1:7;
[.b,w.[ in B
by A2, A13;
then
[.b,w.[ in the
topology of
Sorgenfrey-line
by A3;
then reconsider V =
[.b,w.[,
U =
[.a,q.[ as
open Subset of
Sorgenfrey-line by A12, PRE_TOPC:def 2;
take
U
;
ex b1 being Element of bool the carrier of Sorgenfrey-line st
( U is open & b1 is open & x in U & not y in U & y in b1 & not x in b1 )take
V
;
( U is open & V is open & x in U & not y in U & y in V & not x in V )thus
(
U is
open &
V is
open )
;
( x in U & not y in U & y in V & not x in V )thus
(
x in U & not
y in U &
y in V & not
x in V )
by A10, A13, A14, A11, XXREAL_1:3;
verum end;