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 Element of 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;
then reconsider B = B as prebasis of Sorgenfrey-line by YELLOW_9:27;

now

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 A4: ( x in V & V in B ) ; :: thesis: ex f being continuous Function of Sorgenfrey-line ,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} )
then consider a, q being Real such that
A5: ( V = [.a,q.[ & a < q & q is rational ) by A3;
consider f being continuous Function of Sorgenfrey-line ,I[01] such that
A6: 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 A5, Th62;
take f = f; :: thesis: ( f . x = 0 & f .: (V ` ) c= {1} )
thus f . x = 0 by A4, A5, A6; :: thesis: f .: (V ` ) c= {1}
thus f .: (V ` ) c= {1} :: thesis: verum

proof

let u be set ; :: 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
A7: ( b in V ` & u = f . b ) by FUNCT_2:116;
not b in [.a,q.[ by A5, A7, XBOOLE_0:def 5;
then u = 1 by A6, A7;
hence u in {1} by TARSKI:def 1; :: thesis: verum

end;

end;

hence Sorgenfrey-line is Tychonoff by Th56, Th57; :: thesis: verum