fact: Hypothesis ub_of_chain: forall S:Ensemble T, chain R S -> exists x:T, forall y:T, In S y -> R y x.
imports: Classical ClassicalChoice Relation_Definitions Relation_Definitions_Implicit Ensembles EnsemblesImplicit ProofIrrelevance InverseImage EnsemblesSpec Quotients EnsemblesSpec