fact: Hypothesis lubp : forall X : OF -> CProp, {x : OF | X x} -> {b : OF | is_upper_bound OF X b} -> (forall x y : OF, x[<]y -> is_upper_bound OF X y or {s : OF | X s | x[<]s}) -> l_u_b OF X.
imports: CoRN.reals.Bridges_LUB