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 A st not p = q holds
ex W, V being Subset of A st
( W is open & V is open & p in W & q in V & W misses V )
proof
let p,
q be
Point of
A;
( not p = q implies ex W, V being Subset of A 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 A st
( W is open & V is open & p in W & q in V & W misses V )
reconsider p9 =
p,
q9 =
q as
Point of
T by PRE_TOPC:25;
consider W,
V being
Subset of
T such that A3:
W is
open
and A4:
V is
open
and A5:
(
p9 in W &
q9 in V )
and A6:
W misses V
by A1, A2;
reconsider W9 =
W /\ ([#] A),
V9 =
V /\ ([#] A) as
Subset of
A ;
V in the
topology of
T
by A4;
then A7:
V9 in the
topology of
A
by PRE_TOPC:def 4;
take
W9
;
ex V being Subset of A st
( W9 is open & V is open & p in W9 & q in V & W9 misses V )
take
V9
;
( W9 is open & V9 is open & p in W9 & q in V9 & W9 misses V9 )
W in the
topology of
T
by A3;
then
W9 in the
topology of
A
by PRE_TOPC:def 4;
hence
(
W9 is
open &
V9 is
open )
by A7;
( p in W9 & q in V9 & W9 misses V9 )
thus
(
p in W9 &
q in V9 )
by A5, XBOOLE_0:def 4;
W9 misses V9
A8:
W /\ V = {}
by A6, XBOOLE_0:def 7;
W9 /\ V9 =
(W /\ (V /\ ([#] A))) /\ ([#] A)
by XBOOLE_1:16
.=
{} /\ ([#] A)
by A8, XBOOLE_1:16
.=
{}
;
hence
W9 misses V9
by XBOOLE_0:def 7;
verum
end;
hence
A is T_2
; verum