for ET being FMT_TopSpace
for a being Element of ET
for V being a_neighborhood of a ex O being open Subset of ET st
( a in O & O c= V )