[STATEMENT]
lemma cyclic_on_alldef:
  "cyclic_on f S \<longleftrightarrow> S \<noteq> {} \<and> (\<forall>s\<in>S. S = orbit f s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cyclic_on f S = (S \<noteq> {} \<and> (\<forall>s\<in>S. S = orbit f s))
[PROOF STEP]
unfolding cyclic_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>s\<in>S. S = orbit f s) = (S \<noteq> {} \<and> (\<forall>s\<in>S. S = orbit f s))
[PROOF STEP]
by (auto intro: orbit.step orbit_swap orbit_trans)