fact: Definition is_lub (M:Type) (D : Ensemble M) (lt : relation M) (X:Ensemble M) (a:M) := In _ D a /\ upper_bound D lt X a /\ (forall y, In _ D y -> upper_bound D lt X y -> y = a \/ lt a y).
imports: Coq(Relations Ensembles)