reconsider z = 0 , j = 1, half = 1 / 2 as Element of I[01] by BORSUK_1:40, XXREAL_1:1;
let T be TopSpace; :: thesis: ( T is Tychonoff implies T is regular )
assume A1: for A being closed Subset of T
for a being Point of T st a in A ` holds
ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} ) ; :: according to TOPGEN_5:def 4 :: thesis: T is regular
reconsider A = [.z,half.[, B = ].half,j.] as Subset of I[01] by BORSUK_1:40, XXREAL_1:35, XXREAL_1:36;
reconsider A = A, B = B as open Subset of I[01] by TOPALG_1:4, TOPALG_1:5;
let p be Point of T; :: according to PRE_TOPC:def 11 :: thesis: for b<sub>1</sub> being Element of bool the carrier of T holds
( not b<sub>1</sub> is closed or not p in b<sub>1</sub> ` or ex b₂, b₃ being Element of bool the carrier of T st
( b₂ is open & b₃ is open & p in b₂ & b₁ c= b₃ & b₂ misses b₃ ) )
let P be Subset of T; :: thesis: ( not P is closed or not p in P ` or ex b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of T st
( b<sub>1</sub> is open & b<sub>2</sub> is open & p in b<sub>1</sub> & P c= b<sub>2</sub> & b<sub>1</sub> misses b<sub>2</sub> ) )
assume that
A2: P is closed and
A3: p in P ` ; :: thesis: ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & P c= b₂ & b₁ misses b₂ )
consider f being continuous Function of T,I[01] such that
A4: f . p = 0 and
A5: f .: P c= {1} by A2, A3, A1;
take W = f " A; :: thesis: ex b₁ being Element of bool the carrier of T st
( W is open & b₁ is open & p in W & P c= b₁ & W misses b₁ )
take V = f " B; :: thesis: ( W is open & V is open & p in W & P c= V & W misses V )
[#] I[01] <> {} ;
hence ( W is open & V is open ) by TOPS_2:43; :: thesis: ( p in W & P c= V & W misses V )
0 in A by XXREAL_1:3;
hence p in W by A3, A4, FUNCT_2:38; :: thesis: ( P c= V & W misses V )
A6: dom f = the carrier of T by FUNCT_2:def 1;
1 in B by XXREAL_1:2;
then {1} c= B by ZFMISC_1:31;
then f .: P c= B by A5;
hence P c= V by A6, FUNCT_1:93; :: thesis: W misses V
assume W meets V ; :: thesis: contradiction
then consider x being object such that
A7: x in W and
A8: x in V by XBOOLE_0:3;
A9: f . x in A by A7, FUNCT_1:def 7;
then reconsider fx = f . x as Element of I[01] ;
A10: fx < half by A9, XXREAL_1:3;
f . x in B by A8, FUNCT_1:def 7;
hence contradiction by A10, XXREAL_1:2; :: thesis: verum