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