let seq be Real_Sequence; :: thesis: ( seq is non-decreasing implies for n being Element of NAT holds seq . 0 <= seq . n )
assume A1: seq is non-decreasing ; :: thesis: for n being Element of NAT holds seq . 0 <= seq . n
let n be Element of NAT ; :: thesis: seq . 0 <= seq . n
0 <= n by NAT_1:2;
hence seq . 0 <= seq . n by A1, Th12; :: thesis: verum