let T be non empty TopSpace; :: thesis: ( T is T_2 & T is paracompact implies T is regular )
assume A1:
T is T_2
; :: thesis: ( not T is paracompact or T is regular )
assume A2:
T is paracompact
; :: thesis: T is regular
for x being Point of T
for A being Subset of T st A <> {} & A is closed & x in A ` holds
ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V )
proof
let x be
Point of
T;
:: thesis: for A being Subset of T st A <> {} & A is closed & x in A ` holds
ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V )let A be
Subset of
T;
:: thesis: ( A <> {} & A is closed & x in A ` implies ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V ) )
assume that
A <> {}
and A3:
A is
closed
and A4:
x in A `
;
:: thesis: ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V )
set B =
{x};
A5:
not
x in A
by A4, XBOOLE_0:def 5;
A6:
{x} is
closed
by A1;
A7:
{x} misses A
for
y being
Point of
T st
y in A holds
ex
V,
W being
Subset of
T st
(
V is
open &
W is
open &
{x} c= V &
y in W &
V misses W )
proof
let y be
Point of
T;
:: thesis: ( y in A implies ex V, W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W ) )
assume
y in A
;
:: thesis: ex V, W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W )
then consider V,
W being
Subset of
T such that A8:
V is
open
and A9:
W is
open
and A10:
x in V
and A11:
y in W
and A12:
V misses W
by A1, A5, PRE_TOPC:def 16;
take
V
;
:: thesis: ex W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W )
take
W
;
:: thesis: ( V is open & W is open & {x} c= V & y in W & V misses W )
thus
(
V is
open &
W is
open &
{x} c= V &
y in W &
V misses W )
by A8, A9, A10, A11, A12, ZFMISC_1:37;
:: thesis: verum
end;
then consider Y,
Z being
Subset of
T such that A13:
Y is
open
and A14:
Z is
open
and A15:
{x} c= Y
and A16:
A c= Z
and A17:
Y misses Z
by A2, A3, A6, A7, Th26;
take
Y
;
:: thesis: ex V being Subset of T st
( Y is open & V is open & x in Y & A c= V & Y misses V )
take
Z
;
:: thesis: ( Y is open & Z is open & x in Y & A c= Z & Y misses Z )
thus
(
Y is
open &
Z is
open &
x in Y &
A c= Z &
Y misses Z )
by A13, A14, A15, A16, A17, ZFMISC_1:37;
:: thesis: verum
end;
hence
T is regular
by COMPTS_1:def 5; :: thesis: verum