:: deftheorem defines .: PETRI:def 15 :
for PTN being Petri_net
for S0 being Subset of the carrier of (PTN .:) holds .: S0 = S0;