:: deftheorem defines locally_finite PCOMPS_1:def 1 :
for T being TopStruct
for IT being Subset-Family of T holds
( IT is locally_finite iff for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in IT & V meets W ) } is finite ) );