let T be non empty TopSpace; :: thesis: 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; :: thesis: ( T is T_2 implies A is T_2 )

assume A1: T is T_2 ; :: thesis: 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 )

A is T_2

let A be non empty SubSpace of T; :: thesis: ( T is T_2 implies A is T_2 )

assume A1: T is T_2 ; :: thesis: 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

hence
A is T_2
; :: thesis: verum
let p, q be Point of A; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex V being Subset of A st

( W9 is open & V is open & p in W9 & q in V & W9 misses V )

take V9 ; :: thesis: ( 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; :: thesis: ( p in W9 & q in V9 & W9 misses V9 )

thus ( p in W9 & q in V9 ) by A5, XBOOLE_0:def 4; :: thesis: 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; :: thesis: verum

end;( W is open & V is open & p in W & q in V & W misses V ) )

assume A2: not p = q ; :: thesis: 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 ; :: thesis: ex V being Subset of A st

( W9 is open & V is open & p in W9 & q in V & W9 misses V )

take V9 ; :: thesis: ( 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; :: thesis: ( p in W9 & q in V9 & W9 misses V9 )

thus ( p in W9 & q in V9 ) by A5, XBOOLE_0:def 4; :: thesis: 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; :: thesis: verum