:: deftheorem defines NeighSp FINTOPO2:def 7 :
for T being non empty TopStruct
for b₂ being non empty strict FMT_Space_Str holds
( b₂ = NeighSp T iff ( the carrier of b₂ = the carrier of T & ( for x being Point of b₂ holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) );