hence ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) by A1, Th19; :: thesis:

end;

set S = the carrier of T;
set L = the carrier of R^1;
1 in REAL by XREAL_0:def 1;
then reconsider r = 1 as Element of the carrier of R^1 by TOPMETR:17;
defpred S₁[ set , set ] means $2 = r;
A3: for x being Element of the carrier of T ex y being Element of the carrier of R^1 st S₁[x,y] ;
ex F being Function of the carrier of T, the carrier of R^1 st
for x being Element of the carrier of T holds S₁[x,F . x] from FUNCT_2:sch 3(A3);
then consider F being Function of the carrier of T, the carrier of R^1 such that
A4: for x being Element of the carrier of T holds F . x = r ;
take F ; :: thesis:
A5: dom F = the carrier of T by FUNCT_2:def 1;
thus F is continuous :: thesis:

the carrier of T c= the carrier of T ;
then reconsider O1 = the carrier of T as Subset of T ;
reconsider O2 = {} as Subset of T by XBOOLE_1:2;
let P be Subset of R^1; :: according to PRE_TOPC:def 6 :: thesis:
assume P is closed ; :: thesis:
A6: O2 is closed ;

end;

then for x being object holds
( x in {} iff ( x in dom F & F . x in P ) ) by A4, A5;
hence K433( the carrier of T, the carrier of R^1,F,P) is closed by A6, FUNCT_1:def 7; :: thesis:

end;

let x be Point of T; :: thesis:
thus ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) by A2, A4; :: thesis:

end;