theorem :: PRE_TOPC:24

for T being TopStruct
for A being Subset of T
for p being Point of T holds
( p in Cl A iff ( not T is empty & ( for G being Subset of T st G is open & p in G holds
A meets G ) ) ) by Def7;