take PetriNet ; :: thesis: PetriNet is With_directed_path
thus PetriNet is With_directed_path ; :: thesis: verum