let T be non empty TopSpace; ( ( 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} )
; T is normal
let W, V be Subset of T; COMPTS_1:def 3 ( 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 )
; 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)))
; 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)))
; ( 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; ( 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)))
( 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))) )
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)))
f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2)))
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; verum