take PetriNet ; :: thesis: ( PetriNet is With_directed_circuit & PetriNet is Petri & PetriNet is decision_free_like )
thus ( PetriNet is With_directed_circuit & PetriNet is Petri & PetriNet is decision_free_like ) ; :: thesis: verum