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 3 :: thesis: ( W = {} or V = {} or not W is closed or not V is closed or not W misses V or ex b1, b2 being Element of K10( the carrier of T) st
( b1 is open & b2 is open & W c= b1 & V c= b2 & b1 misses b2 ) )
assume ( W <> {} & V <> {} & W is closed & V is closed & W misses V ) ; :: thesis: ex b1, b2 being Element of K10( the carrier of T) st
( b1 is open & b2 is open & W c= b1 & V c= b2 & b1 misses b2 )
then consider f being continuous Function of T,R^1 such that
A2: f .: W = {0} and
A3: f .: V = {1} by A1;
set Q = f " (R^1 (right_open_halfline (1 / 2)));
set P = f " (R^1 (left_open_halfline (1 / 2)));
take f " (R^1 (left_open_halfline (1 / 2))) ; :: thesis: ex b1 being Element of K10( the carrier of T) st
( f " (R^1 (left_open_halfline (1 / 2))) is open & b1 is open & W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= b1 & f " (R^1 (left_open_halfline (1 / 2))) misses b1 )
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:43; :: 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))) )
A4: R^1 (left_open_halfline (1 / 2)) = left_open_halfline (1 / 2) by TOPREALB:def 3;
A5: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in W or a in f " (R^1 (left_open_halfline (1 / 2))) )
A6: 0 in left_open_halfline (1 / 2) by XXREAL_1:233;
assume A7: a in W ; :: thesis: a in f " (R^1 (left_open_halfline (1 / 2)))
then f . a in f .: W by FUNCT_2:35;
then f . a = 0 by A2, TARSKI:def 1;
hence a in f " (R^1 (left_open_halfline (1 / 2))) by A4, A5, A7, A6, FUNCT_1:def 7; :: thesis: verum
end;
A8: R^1 (right_open_halfline (1 / 2)) = right_open_halfline (1 / 2) by TOPREALB:def 3;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in V or a in f " (R^1 (right_open_halfline (1 / 2))) )
A9: 1 in right_open_halfline (1 / 2) by XXREAL_1:235;
assume A10: a in V ; :: thesis: a in f " (R^1 (right_open_halfline (1 / 2)))
then f . a in f .: V by FUNCT_2:35;
then f . a = 1 by A3, TARSKI:def 1;
hence a in f " (R^1 (right_open_halfline (1 / 2))) by A8, A5, A10, A9, FUNCT_1:def 7; :: thesis: verum
end;
thus f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) by A4, A8, FUNCT_1:71, XXREAL_1:275; :: thesis: verum