not the T-S_Arcs of PTN ~ is empty ;
hence not the S-T_Arcs of (PTN .:) is empty ; :: according to PETRI:def 1 :: thesis: ( PTN .: is with_T-S_arc & not PTN .: is empty & not PTN .: is void )
not the S-T_Arcs of PTN ~ is empty ;
hence not the T-S_Arcs of (PTN .:) is empty ; :: according to PETRI:def 2 :: thesis: ( not PTN .: is empty & not PTN .: is void )
thus ( not PTN .: is empty & not PTN .: is void ) ; :: thesis: verum