:: deftheorem defines closed WAYBEL12:def 1 :
for T being TopStruct
for P being Subset of T holds
( P is closed iff P ` is open );