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 ; :: 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 S1[ 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 S1[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 S1[x,F . x] from 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 K433( the carrier of T, the carrier of R^1,F,P) is closed )
assume P is closed ; :: thesis: K433( 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: K433( 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 ;
hence K433( 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: K433( 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 K433( the carrier of T, the carrier of R^1,F,P) is closed by ; :: 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;