fact: Definition minimal_element_property : Prop := forall S:Ensemble T, Inhabited S -> exists x:T, In S x /\ forall y:T, In S y -> ~ R y x.
imports: Classical Ensembles EnsemblesImplicit Relation_Definitions Relation_Definitions_Implicit EnsemblesSpec