:: deftheorem Def1 defines with_S-T_arc PETRI:def 1 :
for N being PT_net_Str holds
( N is with_S-T_arc iff not the S-T_Arcs of N is empty );