reals_complete_more[T: TYPE FROM real]: THEORY
BEGIN

  IMPORTING  bound_defs[real,T]

  real_complete2: LEMMA   % this could replace real_complete in prelude
    (FORALL (S: (nonempty?[T])):
      (EXISTS (y: real): upper_bound(<=)(y, S)) IMPLIES
        (EXISTS (x: real): least_upper_bound(<=)(x, S)))

  real_lower_complete2: LEMMA % this could replace real_complete in prelude
    (FORALL (S: (nonempty?[T])):
      (EXISTS (y : real): lower_bound(<=)(y, S)) IMPLIES 
        (EXISTS (x: real): greatest_lower_bound(<=)(x, S)))


END reals_complete_more