let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & 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 <> {} & 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 <> {} & 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 ) ) ) )
set R = the Rain of A,B;
take Thunder the Rain of A,B ; :: thesis: ( Thunder the Rain of A,B is continuous & ( for x being Point of T holds
( 0 <= (Thunder the Rain of A,B) . x & (Thunder the Rain of A,B) . x <= 1 & ( x in A implies (Thunder the Rain of A,B) . x = 0 ) & ( x in B implies (Thunder the Rain of A,B) . x = 1 ) ) ) )
thus ( Thunder the Rain of A,B is continuous & ( for x being Point of T holds
( 0 <= (Thunder the Rain of A,B) . x & (Thunder the Rain of A,B) . x <= 1 & ( x in A implies (Thunder the Rain of A,B) . x = 0 ) & ( x in B implies (Thunder the Rain of A,B) . x = 1 ) ) ) ) by A1, Th18; :: thesis: verum