let seq be Real_Sequence; :: thesis: ( seq is V89() & seq is nonnegative implies lower_bound seq >= 0 )
assume ( seq is V89() & 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