set X = Sorgenfrey-line ;
A1:
the carrier of Sorgenfrey-line = REAL
by TOPGEN_3:def 2;
consider B being Subset-Family of REAL such that
A2:
the topology of Sorgenfrey-line = UniCl B
and
A3:
B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) }
by TOPGEN_3:def 2;
B c= UniCl B
by CANTOR_1:1;
then
B is Basis of Sorgenfrey-line
by A1, A2, CANTOR_1:def 2, TOPS_2:64;
then reconsider B = B as prebasis of Sorgenfrey-line by YELLOW_9:27;
now for x being Point of Sorgenfrey-line
for V being Subset of Sorgenfrey-line st x in V & V in B holds
ex f being continuous Function of Sorgenfrey-line,I[01] st
( f . x = 0 & f .: (V `) c= {1} )let x be
Point of
Sorgenfrey-line;
for V being Subset of Sorgenfrey-line st x in V & V in B holds
ex f being continuous Function of Sorgenfrey-line,I[01] st
( f . x = 0 & f .: (V `) c= {1} )let V be
Subset of
Sorgenfrey-line;
( x in V & V in B implies ex f being continuous Function of Sorgenfrey-line,I[01] st
( f . x = 0 & f .: (V `) c= {1} ) )assume that A4:
x in V
and A5:
V in B
;
ex f being continuous Function of Sorgenfrey-line,I[01] st
( f . x = 0 & f .: (V `) c= {1} )consider a,
q being
Real such that A6:
V = [.a,q.[
and
a < q
and A7:
q is
rational
by A5, A3;
consider f being
continuous Function of
Sorgenfrey-line,
I[01] such that A8:
for
b being
Point of
Sorgenfrey-line holds
( (
b in [.a,q.[ implies
f . b = 0 ) & ( not
b in [.a,q.[ implies
f . b = 1 ) )
by A7, Th58;
take f =
f;
( f . x = 0 & f .: (V `) c= {1} )thus
f . x = 0
by A4, A6, A8;
f .: (V `) c= {1}thus
f .: (V `) c= {1}
verum end;
hence
Sorgenfrey-line is Tychonoff
by Th52, Th53; verum