theorem Th7: :: NAGATA_1:7

for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial )