[STATEMENT]
lemma finite_polytope_facets:
  assumes "polytope S"
  shows "finite {T. T facet_of S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {T. T facet_of S}
[PROOF STEP]
by (simp add: assms facet_of_def finite_polytope_faces)