:: deftheorem Def2 defines with_T-S_arc PETRI:def 2 :
for N being PT_net_Str holds
( N is with_T-S_arc iff not the T-S_Arcs of N is empty );