let T be non empty T_2 TopSpace; Top2NTop T is T_2 NTopSpace
reconsider NT = Top2NTop T as NTopSpace ;
now for F being Filter of the carrier of NT holds lim_filter F is trivial let F be
Filter of the
carrier of
NT;
lim_filter F is trivial set S =
{ x where x is Point of NT : F is_filter-finer_than U_FMT x } ;
for
x,
y being
object holds
( not
x in lim_filter F or not
y in lim_filter F or not
x <> y )
proof
let x,
y be
object ;
( not x in lim_filter F or not y in lim_filter F or not x <> y )
assume that A1:
x in lim_filter F
and A2:
y in lim_filter F
and A3:
x <> y
;
contradiction
consider x9 being
Point of
NT such that A4:
x = x9
and A5:
F is_filter-finer_than U_FMT x9
by A1;
consider y9 being
Point of
NT such that A6:
y = y9
and A7:
F is_filter-finer_than U_FMT y9
by A2;
reconsider x99 =
x9,
y99 =
y9 as
Point of
T by FINTOPO7:def 15;
consider G1,
G2 being
Subset of
T such that A8:
G1 is
open
and A9:
G2 is
open
and A10:
x99 in G1
and A11:
y99 in G2
and A12:
G1 misses G2
by A4, A6, A3, PRE_TOPC:def 10;
reconsider G19 =
G1,
G29 =
G2 as
open Subset of
NT by A8, A9, Lm1;
A13:
(
G19 in U_FMT x9 &
G29 in U_FMT y9 )
by A10, A11, FINTOPO7:def 1;
(
U_FMT x9 c= F &
U_FMT y9 c= F )
by A5, A7, CARDFIL2:def 6;
then
G19 /\ G29 in F
by A13, CARD_FIL:def 1;
hence
contradiction
by A12, CARD_FIL:def 1;
verum
end; hence
lim_filter F is
trivial
;
verum end;
then
NT is T_2
;
hence
Top2NTop T is T_2 NTopSpace
; verum