:: deftheorem Def2 defines open PRE_TOPC:def 2 :
for T being TopStruct
for P being Subset of T holds
( P is open iff P in the topology of T );