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