:: deftheorem defines e_Transitions E_SIEC:def 10 :
for N being e_net holds e_Transitions N = the carrier of N \ (e_Places N);