proposition: Theorem Only_DN_or_UP : forall F : R -> Prop, forall x fd fu f : R, Rnd_DN_pt F x fd -> Rnd_UP_pt F x fu -> F f -> (fd <= f <= fu)%R -> f = fd \/ f = fu.
proof: Proof. intros F x fd fu f Hd Hu Hf [Hdf Hfu]. destruct (Rle_or_lt x f) ; [right|left]. apply Rle_antisym with (1 := Hfu). now apply Hu. apply Rlt_le in H. apply Rle_antisym with (2 := Hdf). now apply Hd. Qed.
imports: Coq(Reals) Raux Defs