let T be non empty TopSpace; :: thesis: ( ( for A, B being non empty closed Subset of T st A misses B holds
ex f being continuous Function of T,R^1 st
( f .: A = {0 } & f .: B = {1} ) ) implies T is normal )
assume A1: for A, B being non empty closed Subset of T st A misses B holds
ex f being continuous Function of T,R^1 st
( f .: A = {0 } & f .: B = {1} ) ; :: thesis: T is normal
let W, V be Subset of T; :: according to COMPTS_1:def 6 :: thesis: ( W = {} or V = {} or not W is closed or not V is closed or not W misses V or ex b₁, b₂ being Element of K21(the carrier of T) st
( b₁ is open & b₂ is open & W c= b₁ & V c= b₂ & b₁ misses b₂ ) )
assume that
A2: ( W <> {} & V <> {} ) and
A3: ( W is closed & V is closed ) and
A4: W misses V ; :: thesis: ex b₁, b₂ being Element of K21(the carrier of T) st
( b₁ is open & b₂ is open & W c= b₁ & V c= b₂ & b₁ misses b₂ )
consider f being continuous Function of T,R^1 such that
A5: f .: W = {0 } and
A6: f .: V = {1} by A1, A2, A3, A4;
set P = f " (R^1 (left_open_halfline (1 / 2)));
set Q = f " (R^1 (right_open_halfline (1 / 2)));
A7: R^1 (left_open_halfline (1 / 2)) = left_open_halfline (1 / 2) by TOPREALB:def 3;
A8: R^1 (right_open_halfline (1 / 2)) = right_open_halfline (1 / 2) by TOPREALB:def 3;
take f " (R^1 (left_open_halfline (1 / 2))) ; :: thesis: ex b₁ being Element of K21(the carrier of T) st
( f " (R^1 (left_open_halfline (1 / 2))) is open & b₁ is open & W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= b₁ & f " (R^1 (left_open_halfline (1 / 2))) misses b₁ )
take f " (R^1 (right_open_halfline (1 / 2))) ; :: thesis: ( f " (R^1 (left_open_halfline (1 / 2))) is open & f " (R^1 (right_open_halfline (1 / 2))) is open & W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= f " (R^1 (right_open_halfline (1 / 2))) & f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) )
[#] R^1 <> {} ;
hence ( f " (R^1 (left_open_halfline (1 / 2))) is open & f " (R^1 (right_open_halfline (1 / 2))) is open ) by TOPS_2:55; :: thesis: ( W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= f " (R^1 (right_open_halfline (1 / 2))) & f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) )
A9: dom f = the carrier of T by FUNCT_2:def 1;
thus W c= f " (R^1 (left_open_halfline (1 / 2))) :: thesis: ( V c= f " (R^1 (right_open_halfline (1 / 2))) & f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) )

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in W or a in f " (R^1 (left_open_halfline (1 / 2))) )
assume A10: a in W ; :: thesis: a in f " (R^1 (left_open_halfline (1 / 2)))
then f . a in f .: W by FUNCT_2:43;
then A11: f . a = 0 by A5, TARSKI:def 1;
0 in left_open_halfline (1 / 2) by XXREAL_1:233;
hence a in f " (R^1 (left_open_halfline (1 / 2))) by A7, A9, A10, A11, FUNCT_1:def 13; :: thesis: verum

end;

thus V c= f " (R^1 (right_open_halfline (1 / 2))) :: thesis: f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2)))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in V or a in f " (R^1 (right_open_halfline (1 / 2))) )
assume A12: a in V ; :: thesis: a in f " (R^1 (right_open_halfline (1 / 2)))
then f . a in f .: V by FUNCT_2:43;
then A13: f . a = 1 by A6, TARSKI:def 1;
1 in right_open_halfline (1 / 2) by XXREAL_1:235;
hence a in f " (R^1 (right_open_halfline (1 / 2))) by A8, A9, A12, A13, FUNCT_1:def 13; :: thesis: verum

end;

thus f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) by A7, A8, FUNCT_1:141, XXREAL_1:275; :: thesis: verum