:: deftheorem defines f_transitions FF_SIEC:def 12 :
for M being Pnet holds f_transitions M = the carrier' of M;