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