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 ) ) ) )
consider R being Rain of A,B;
take Thunder R ; :: thesis: ( Thunder R is continuous & ( for x being Point of T holds
( 0 <= (Thunder R) . x & (Thunder R) . x <= 1 & ( x in A implies (Thunder R) . x = 0 ) & ( x in B implies (Thunder R) . x = 1 ) ) ) )
thus ( Thunder R is continuous & ( for x being Point of T holds
( 0 <= (Thunder R) . x & (Thunder R) . x <= 1 & ( x in A implies (Thunder R) . x = 0 ) & ( x in B implies (Thunder R) . x = 1 ) ) ) ) by A1, Th21; :: thesis: verum