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