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 :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( f . x = 0 & f .: (V `) c= {1} )
thus f . x = 0 by A4, A6, A8; :: thesis: f .: (V `) c= {1}
thus f .: (V `) c= {1} :: thesis: verum

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in f .: (V `) or u in {1} )
assume u in f .: (V `) ; :: thesis: u in {1}
then consider b being Point of Sorgenfrey-line such that
A9: b in V ` and
A10: u = f . b by FUNCT_2:65;
not b in [.a,q.[ by A6, A9, XBOOLE_0:def 5;
then u = 1 by A8, A10;
hence u in {1} by TARSKI:def 1; :: thesis: verum

end;

end;

hence Sorgenfrey-line is Tychonoff by Th52, Th53; :: thesis: verum