fact: Definition complete I A (M:family I A) := forall K u, downward_closed M K -> coherent M K u -> exists l, limit M K u l.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)