let T be non empty homogeneous TopSpace; ( 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 )
given p being Point of T such that A1:
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 )
; T is regular
A2:
[#] T <> {}
;
now for A being open Subset of T
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 A be
open Subset of
T;
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;
( q in A implies ex fB being open Subset of T st
( q in fB & Cl fB c= A ) )assume A3:
q in A
;
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;
A5:
f " A is
open
by A2, TOPS_2:43;
reconsider g =
f as
Function ;
A6:
dom f = the
carrier of
T
by FUNCT_2:def 1;
A7:
rng f = [#] T
by TOPS_2:def 5;
then
(
(g ") . q = (f ") . q &
g . ((g ") . q) in A )
by A3, FUNCT_1:32;
then A8:
(g ") . q in g " A
by A6, FUNCT_1:def 7;
p = (g ") . q
by A4, A6, FUNCT_1:32;
then consider B being
Subset of
T such that A9:
p in B
and A10:
B is
open
and A11:
Cl B c= f " A
by A1, A8, A5;
reconsider fB =
f .: B as
open Subset of
T by A10, Th24;
take fB =
fB;
( q in fB & Cl fB c= A )thus
q in fB
by A4, A6, A9, FUNCT_1:def 6;
Cl fB c= AA12:
f .: (Cl B) = Cl fB
by TOPS_2:60;
f .: (Cl B) c= f .: (f " A)
by A11, RELAT_1:123;
hence
Cl fB c= A
by A7, A12, FUNCT_1:77;
verum end;
hence
T is regular
by URYSOHN1:21; verum