:: deftheorem defines Outbds PETRI_2:def 10 :
for CPNT1 being Colored_Petri_net holds Outbds CPNT1 = { x where x is transition of CPNT1 : x is outbound } ;