let T be TopSpace; :: thesis: ( T is Tychonoff implies T is regular )
assume A2: 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
let p be Point of T; :: according to PRE_TOPC:def 17 :: 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₃ & not b₂ meets 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> & not b<sub>1</sub> meets b<sub>2</sub> ) )
assume A3: ( P is closed & 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₂ & not b₁ meets b₂ )
then consider f being continuous Function of T,I[01] such that
A4: ( f . p = 0 & f .: P c= {1} ) by A2;
reconsider z = 0 , j = 1, half = 1 / 2 as Element of I[01] by BORSUK_1:83, XXREAL_1:1;
reconsider A = [.z,half.[, B = ].half,j.] as Subset of I[01] by BORSUK_1:83, XXREAL_1:35, XXREAL_1:36;
reconsider A = A, B = B as open Subset of I[01] by TOPALG_1:4, TOPALG_1:5;
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₁ & not W meets b₁ )
take V = f " B; :: thesis: ( W is open & V is open & p in W & P c= V & not W meets V )
[#] I[01] <> {} ;
hence ( W is open & V is open ) by TOPS_2:55; :: thesis: ( p in W & P c= V & not W meets V )
0 in A by XXREAL_1:3;
hence p in W by A3, A4, FUNCT_2:46; :: thesis: ( P c= V & not W meets V )
1 in B by XXREAL_1:2;
then {1} c= B by ZFMISC_1:37;
then ( f .: P c= B & dom f = the carrier of T ) by A4, FUNCT_2:def 1, XBOOLE_1:1;
hence P c= V by FUNCT_1:163; :: thesis: not W meets V
assume W meets V ; :: thesis: contradiction
then consider x being set such that
A5: ( x in W & x in V ) by XBOOLE_0:3;
A6: ( f . x in A & f . x in B ) by A5, FUNCT_1:def 13;
then reconsider fx = f . x as Element of I[01] ;
( fx < half & fx > half ) by A6, XXREAL_1:2, XXREAL_1:3;
hence contradiction ; :: thesis: verum