theorem Th9: :: TOPGEN_1:9

for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p in Fr A iff for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) )