for ET being FMT_TopSpace
for A being non empty Subset of ET
for V being Subset of ET holds
( V is a_neighborhood of A iff ex O being open Subset of ET st
( A c= O & O c= V ) )