let seq be Real_Sequence; :: thesis: ( seq is bounded_above & seq is nonnegative implies upper_bound seq >= 0 )
assume A1: ( seq is bounded_above & seq is nonnegative ) ; :: thesis: upper_bound seq >= 0
then seq . 0 <= upper_bound seq by Th7;
hence upper_bound seq >= 0 by A1, Def3; :: thesis: verum