fact: Definition chain (S: Ensemble T) : Prop := forall x y:T, In S x -> In S y -> (R x y \/ R y x).
imports: Classical ClassicalChoice Relation_Definitions Relation_Definitions_Implicit Ensembles EnsemblesImplicit ProofIrrelevance InverseImage EnsemblesSpec Quotients