set NT = NeighSp T;

for x being Element of (NeighSp T)

for D being Subset of (NeighSp T) st D in U_FMT x holds

x in D

for x being Element of (NeighSp T)

for D being Subset of (NeighSp T) st D in U_FMT x holds

x in D

proof

hence
NeighSp T is Fo_filled
; :: thesis: verum
let x be Element of (NeighSp T); :: thesis: for D being Subset of (NeighSp T) st D in U_FMT x holds

x in D

let D be Subset of (NeighSp T); :: thesis: ( D in U_FMT x implies x in D )

assume A1: D in U_FMT x ; :: thesis: x in D

U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by FINTOPO2:def 7;

then consider V0 being Subset of T such that

A2: D = V0 and

V0 in the topology of T and

A3: x in V0 by A1;

thus x in D by A2, A3; :: thesis: verum

end;x in D

let D be Subset of (NeighSp T); :: thesis: ( D in U_FMT x implies x in D )

assume A1: D in U_FMT x ; :: thesis: x in D

U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by FINTOPO2:def 7;

then consider V0 being Subset of T such that

A2: D = V0 and

V0 in the topology of T and

A3: x in V0 by A1;

thus x in D by A2, A3; :: thesis: verum