fact: Definition maximal (x:T) : Prop := forall y:T, R x y -> x = y.
imports: Classical ClassicalChoice Relation_Definitions Relation_Definitions_Implicit Ensembles EnsemblesImplicit ProofIrrelevance InverseImage EnsemblesSpec Quotients