set X = Sorgenfrey-line ;
let x be real number ; :: thesis: for w being rational number st x < w holds
ex f being continuous Function of Sorgenfrey-line ,I[01] st
for a being Point of Sorgenfrey-line holds
( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )
let w be rational number ; :: thesis: ( x < w implies ex f being continuous Function of Sorgenfrey-line ,I[01] st
for a being Point of Sorgenfrey-line holds
( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) ) )
assume x < w ; :: thesis: ex f being continuous Function of Sorgenfrey-line ,I[01] st
for a being Point of Sorgenfrey-line holds
( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )
defpred S₁[ set ] means $1 in [.x,w.[;
deffunc H₁( set ) -> Element of NAT = 0 ;
deffunc H₂( set ) -> Element of NAT = 1;
A1: for a being set st a in the carrier of Sorgenfrey-line holds
( ( S₁[a] implies H₁(a) in the carrier of I[01] ) & ( not S₁[a] implies H₂(a) in the carrier of I[01] ) ) by BORSUK_1:83, XXREAL_1:1;
consider f being Function of Sorgenfrey-line ,I[01] such that
A2: for a being set st a in the carrier of Sorgenfrey-line holds
( ( S₁[a] implies f . a = H₁(a) ) & ( not S₁[a] implies f . a = H₂(a) ) ) from FUNCT_2:sch 5(A1);
reconsider V = [.x,w.[ as open closed Subset of Sorgenfrey-line by Th61, TOPGEN_3:11;
reconsider 00 = 0 , 01 = 1 as Element of I[01] by BORSUK_1:83, XXREAL_1:1;
reconsider f1 = (Sorgenfrey-line | V) --> 00 as continuous Function of (Sorgenfrey-line | V),I[01] ;
reconsider f2 = (Sorgenfrey-line | (V ` )) --> 01 as continuous Function of (Sorgenfrey-line | (V ` )),I[01] ;
A3: ( [#] Sorgenfrey-line = the carrier of Sorgenfrey-line & the carrier of (Sorgenfrey-line | V) = V & the carrier of (Sorgenfrey-line | (V ` )) = V ` ) by PRE_TOPC:29;
then A4: ( dom f = [#] Sorgenfrey-line & dom f1 = V & dom f2 = V ` ) by FUNCT_2:def 1;
A5: V \/ (V ` ) = [#] Sorgenfrey-line by PRE_TOPC:18;

now

let u be set ; :: thesis: ( u in (dom f1) \/ (dom f2) implies ( ( u in dom f2 implies f . u = f2 . u ) & ( not u in dom f2 implies f . u = f1 . u ) ) )
assume u in (dom f1) \/ (dom f2) ; :: thesis: ( ( u in dom f2 implies f . u = f2 . u ) & ( not u in dom f2 implies f . u = f1 . u ) )
then reconsider x = u as Point of Sorgenfrey-line by A4, PRE_TOPC:18;

hereby :: thesis: ( not u in dom f2 implies f . u = f1 . u )

assume u in dom f2 ; :: thesis: f . u = f2 . u
then ( not x in V & ((V ` ) --> 1) . u = 1 & f2 = (V ` ) --> 1 ) by A3, FUNCOP_1:13, XBOOLE_0:def 5;
hence f . u = f2 . u by A2; :: thesis: verum

end;

assume not u in dom f2 ; :: thesis: f . u = f1 . u
then A6: x in V by A4, SUBSET_1:50;
hence f . u = 0 by A2
.= f1 . u by A3, A6, FUNCOP_1:13 ;
:: thesis: verum

end;

then f = f1 +* f2 by A4, A5, FUNCT_4:def 1;
then reconsider f = f as continuous Function of Sorgenfrey-line ,I[01] by Th16;
take f ; :: thesis: for a being Point of Sorgenfrey-line holds
( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )
let a be Point of Sorgenfrey-line ; :: thesis: ( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )
thus ( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) ) by A2; :: thesis: verum