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 Element of REAL : ( x < q & q is rational ) }
by TOPGEN_3:def 2;
A3:
B c= the topology of Sorgenfrey-line
by A1, CANTOR_1:1;
let x, y be Point of Sorgenfrey-line ; :: according to URYSOHN1:def 9 :: thesis: ( 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 Real by TOPGEN_3:def 2;
assume A4:
x <> y
; :: thesis: 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
;
:: thesis: 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 )then consider w being
rational number such that A6:
(
a < w &
w < b )
by RAT_1:22;
b < b + 1
by XREAL_1:31;
then consider q being
rational number such that A7:
(
b < q &
q < b + 1 )
by RAT_1:22;
(
w is
Real &
q is
Real )
by XREAL_0:def 1;
then
(
[.a,w.[ in B &
[.b,q.[ in B )
by A2, A6, A7;
then
(
[.a,w.[ in the
topology of
Sorgenfrey-line &
[.b,q.[ in the
topology of
Sorgenfrey-line )
by A3;
then reconsider U =
[.a,w.[,
V =
[.b,q.[ as
open Subset of
Sorgenfrey-line by PRE_TOPC:def 5;
take
U
;
:: thesis: 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
;
:: thesis: ( 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 )
;
:: thesis: ( 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, A6, A7, XXREAL_1:3;
:: thesis: verum end; suppose A8:
a > b
;
:: thesis: 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 )then consider w being
rational number such that A9:
(
b < w &
w < a )
by RAT_1:22;
a < a + 1
by XREAL_1:31;
then consider q being
rational number such that A10:
(
a < q &
q < a + 1 )
by RAT_1:22;
(
w is
Real &
q is
Real )
by XREAL_0:def 1;
then
(
[.b,w.[ in B &
[.a,q.[ in B )
by A2, A9, A10;
then
(
[.b,w.[ in the
topology of
Sorgenfrey-line &
[.a,q.[ in the
topology of
Sorgenfrey-line )
by A3;
then reconsider V =
[.b,w.[,
U =
[.a,q.[ as
open Subset of
Sorgenfrey-line by PRE_TOPC:def 5;
take
U
;
:: thesis: 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
;
:: thesis: ( 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 )
;
:: thesis: ( 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 A8, A9, A10, XXREAL_1:3;
:: thesis: verum end;