:: deftheorem Def7 defines Cl PRE_TOPC:def 7 :
for GX being TopStruct
for A, b₃ being Subset of GX holds
( b₃ = Cl A iff for p being set st p in the carrier of GX holds
( p in b₃ iff for G being Subset of GX st G is open & p in G holds
A meets G ) );