:: deftheorem Def3 defines correct YELLOW13:def 3 :
for T being TopStruct
for p being Point of T
for P being basis of p holds
( P is correct iff for A being Subset of T holds
( A in P iff p in Int A ) );