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