let NT be T_2 NTopSpace; NTop2Top NT is non empty strict T_2 TopSpace
reconsider T = NTop2Top NT as non empty TopSpace ;
now for p, q being Point of T st p <> q holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 )let p,
q be
Point of
T;
( p <> q implies ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 ) )assume A1:
p <> q
;
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 )reconsider p9 =
p,
q9 =
q as
Point of
NT by FINTOPO7:def 16;
set Sp =
lim_filter (U_FMT p9);
set Sq =
lim_filter (U_FMT q9);
consider Vx being
Element of
U_FMT p9,
Vy being
Element of
U_FMT q9 such that A2:
Vx misses Vy
by A1, Th39;
p9 is_interior_point_of Vx
by FINTOPO7:def 5;
then consider Ox being
open Subset of
NT such that A3:
p9 in Ox
and A4:
Ox c= Vx
by Lm4;
q9 is_interior_point_of Vy
by FINTOPO7:def 5;
then consider Oy being
open Subset of
NT such that A5:
q9 in Oy
and A6:
Oy c= Vy
by Lm4;
reconsider G1 =
Ox,
G2 =
Oy as
open Subset of
T by Lm9;
G1 misses G2
by A4, A6, A2, XBOOLE_1:64;
hence
ex
G1,
G2 being
Subset of
T st
(
G1 is
open &
G2 is
open &
p in G1 &
q in G2 &
G1 misses G2 )
by A3, A5;
verum end;
hence
NTop2Top NT is non empty strict T_2 TopSpace
by PRE_TOPC:def 10; verum