proposition: Lemma WF_implies_MEP: well_founded R -> minimal_element_property.
proof: Proof. unfold well_founded. unfold minimal_element_property. intros WF S Hinh. destruct Hinh. revert x H. apply (@well_founded_ind T R WF (fun x:T => In S x -> exists y:T, In S y /\ (forall z:T, In S z -> ~ R z y))). intros. case (classic (forall y:T, In S y -> ~ R y x)). - exists x. split. + assumption. + assumption. - intro. apply not_all_ex_not in H1. destruct H1. apply imply_to_and in H1. destruct H1. apply H with x0. + apply NNPP. assumption. + assumption. Qed.
imports: Coq(Classical) ZornsLemma(EnsemblesImplicit) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(EnsemblesSpec)