[STATEMENT]
lemma irreflp_onI [Pure.intro]:
  "(\<And>a. a \<in> A \<Longrightarrow> \<not> P a a) \<Longrightarrow> irreflp_on P A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> A \<Longrightarrow> \<not> P a a) \<Longrightarrow> irreflp_on P A
[PROOF STEP]
unfolding irreflp_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> A \<Longrightarrow> \<not> P a a) \<Longrightarrow> \<forall>a\<in>A. \<not> P a a
[PROOF STEP]
by blast