let T be non empty TopSpace; for A being non empty SubSpace of T st T is T_2 holds
A is T_2
let A be non empty SubSpace of T; ( T is T_2 implies A is T_2 )
assume A1:
T is T_2
; A is T_2
for p, q being Point of st not p = q holds
ex W, V being Subset of st
( W is open & V is open & p in W & q in V & W misses V )
proof
let p,
q be
Point of ;
( not p = q implies ex W, V being Subset of st
( W is open & V is open & p in W & q in V & W misses V ) )
assume A2:
not
p = q
;
ex W, V being Subset of st
( W is open & V is open & p in W & q in V & W misses V )
reconsider p' =
p,
q' =
q as
Point of
by PRE_TOPC:55;
consider W,
V being
Subset of
such that A3:
W is
open
and A4:
V is
open
and A5:
(
p' in W &
q' in V )
and A6:
W misses V
by A1, A2, PRE_TOPC:def 16;
reconsider W' =
W /\ ([#] A),
V' =
V /\ ([#] A) as
Subset of ;
V in the
topology of
T
by A4, PRE_TOPC:def 5;
then A7:
V' in the
topology of
A
by PRE_TOPC:def 9;
take
W'
;
ex V being Subset of st
( W' is open & V is open & p in W' & q in V & W' misses V )
take
V'
;
( W' is open & V' is open & p in W' & q in V' & W' misses V' )
W in the
topology of
T
by A3, PRE_TOPC:def 5;
then
W' in the
topology of
A
by PRE_TOPC:def 9;
hence
(
W' is
open &
V' is
open )
by A7, PRE_TOPC:def 5;
( p in W' & q in V' & W' misses V' )
thus
(
p in W' &
q in V' )
by A5, XBOOLE_0:def 4;
W' misses V'
A8:
W /\ V = {}
by A6, XBOOLE_0:def 7;
W' /\ V' =
(W /\ (V /\ ([#] A))) /\ ([#] A)
by XBOOLE_1:16
.=
{} /\ ([#] A)
by A8, XBOOLE_1:16
.=
{}
;
hence
W' misses V'
by XBOOLE_0:def 7;
verum
end;
hence
A is T_2
by PRE_TOPC:def 16; verum