proposition: Lemma Pinf_unfolded2 : forall c' : OF, inf[<]c' -> {s : OF | seq2set g s | s[<]c'}.
proof: Proof. unfold inf in |- *. elim Pinf. simpl in |- *. intros. rename X into H. elim (b c' H); intros x p; elim p; exists x; auto. Qed.
imports: CoRN.reals.Bridges_LUB