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

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