[STATEMENT]
lemma  nmi_P[no_atp]: "\<forall>x. ~P \<and> P \<longrightarrow>  (\<exists>u\<in> U. u \<le> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<not> P \<and> P \<longrightarrow> (\<exists>u\<in>U. u \<le> x)
[PROOF STEP]
by auto