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 A2: seq . 0 <= upper_bound seq by Th7;
0 <= seq . 0 by A1;
hence upper_bound seq >= 0 by A2; :: thesis: verum