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