[STATEMENT]
lemma Class_revI [intro, simp]:
  "(a, b) \<in> E \<Longrightarrow> b \<in> Class a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> E \<Longrightarrow> b \<in> Class a
[PROOF STEP]
by (blast intro: symmetric)