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