let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A misses B holds
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 ) ) ) )
let A, B be closed Subset of T; :: thesis: ( A misses B implies 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 ) ) ) ) )
assume A1: A misses B ; :: thesis: 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 ) ) ) )

per cases ( A <> {} or A = {} ) ;

suppose A <> {} ; :: thesis: 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 ) ) ) )

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: verum

end;

suppose A2: A = {} ; :: thesis: 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 ) ) ) )

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: ( 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 ) ) ) )
A5: dom F = the carrier of T by FUNCT_2:def 1;
thus F is continuous :: thesis: 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 ) )

proof

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: ( not P is closed or K436( the carrier of T, the carrier of R^1,F,P) is closed )
assume P is closed ; :: thesis: K436( the carrier of T, the carrier of R^1,F,P) is closed
A6: O2 is closed ;

per cases ( 1 in P or not 1 in P ) ;

suppose 1 in P ; :: thesis: K436( the carrier of T, the carrier of R^1,F,P) is closed

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

end;

suppose not 1 in P ; :: thesis: K436( the carrier of T, the carrier of R^1,F,P) is closed

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

end;

end;

end;

let x be Point of T; :: thesis: ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) )
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: verum

end;

end;