take TrivialPetriNet ; :: thesis: ( not TrivialPetriNet is empty & not TrivialPetriNet is void & TrivialPetriNet is with_S-T_arc & TrivialPetriNet is with_T-S_arc & TrivialPetriNet is strict )
thus ( not TrivialPetriNet is empty & not TrivialPetriNet is void & TrivialPetriNet is with_S-T_arc & TrivialPetriNet is with_T-S_arc & TrivialPetriNet is strict ) ; :: thesis: verum