set N = TrivialColoredPetriNet ;
thus not the S-T_Arcs of TrivialColoredPetriNet is empty ; :: according to PETRI:def 1 :: thesis: ( TrivialColoredPetriNet is with_T-S_arc & not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void )
thus not the T-S_Arcs of TrivialColoredPetriNet is empty ; :: according to PETRI:def 2 :: thesis: ( not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void )
thus ( not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void ) ; :: thesis: verum