:: deftheorem defines OpenNeighborhoods FINTOPO7:def 12 :
for ET being FMT_TopSpace
for A being non empty Subset of ET holds OpenNeighborhoods A = { N where N is open a_neighborhood of A : verum } ;