let seq be Real_Sequence; :: thesis: ( seq is bounded_below & seq is nonnegative implies lower_bound seq >= 0 )
assume ( seq is bounded_below & seq is nonnegative ) ; :: thesis: lower_bound seq >= 0
then for n being Element of NAT holds seq . n >= 0 by Def3;
hence lower_bound seq >= 0 by Th10; :: thesis: verum