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