let T be non empty homogeneous TopSpace; :: thesis: ( ex p being Point of T st
for A being Subset of T st A is open & p in A holds
ex B being Subset of T st
( p in B & B is open & Cl B c= A ) implies T is regular )
A1:
[#] T <> {}
;
given p being Point of T such that A2:
for A being Subset of T st A is open & p in A holds
ex B being Subset of T st
( p in B & B is open & Cl B c= A )
; :: thesis: T is regular
now let A be
open Subset of
T;
:: thesis: for q being Point of T st q in A holds
ex fB being open Subset of T st
( q in fB & Cl fB c= A )let q be
Point of
T;
:: thesis: ( q in A implies ex fB being open Subset of T st
( q in fB & Cl fB c= A ) )assume A3:
q in A
;
:: thesis: ex fB being open Subset of T st
( q in fB & Cl fB c= A )consider f being
Homeomorphism of
T such that A4:
f . p = q
by Def6;
reconsider g =
f as
Function ;
A5:
dom f = the
carrier of
T
by FUNCT_2:def 1;
A6:
rng f = [#] T
by TOPS_2:def 5;
A7:
p = (g " ) . q
by A4, A5, FUNCT_1:54;
A8:
(g " ) . q = (f " ) . q
;
g . ((g " ) . q) in A
by A3, A6, FUNCT_1:54;
then A9:
(g " ) . q in g " A
by A5, A8, FUNCT_1:def 13;
f " A is
open
by A1, TOPS_2:55;
then consider B being
Subset of
T such that A10:
(
p in B &
B is
open &
Cl B c= f " A )
by A2, A7, A9;
reconsider fB =
f .: B as
open Subset of
T by A10, Th25;
take fB =
fB;
:: thesis: ( q in fB & Cl fB c= A )thus
q in fB
by A4, A5, A10, FUNCT_1:def 12;
:: thesis: Cl fB c= AA11:
f .: (Cl B) c= f .: (f " A)
by A10, RELAT_1:156;
f .: (Cl B) = Cl fB
by TOPS_2:74;
hence
Cl fB c= A
by A6, A11, FUNCT_1:147;
:: thesis: verum end;
hence
T is regular
by URYSOHN1:29; :: thesis: verum