let r be real number ; :: thesis: for seq being Real_Sequence holds
( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is bounded_below & r <= inf seq ) )
let seq be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is bounded_below & r <= inf seq ) )
thus ( ( for n being Element of NAT holds r <= seq . n ) implies ( seq is bounded_below & r <= inf seq ) ) :: thesis: ( seq is bounded_below & r <= inf seq implies for n being Element of NAT holds r <= seq . n )

proof

assume A1: for n being Element of NAT holds r <= seq . n ; :: thesis: ( seq is bounded_below & r <= inf seq )

now

let m be Element of NAT ; :: thesis: r - 1 < seq . m
r <= seq . m by A1;
hence r - 1 < seq . m by Lm1; :: thesis: verum

end;

hence A2: seq is bounded_below by SEQ_2:def 4; :: thesis: r <= inf seq

now

set r1 = r - (inf seq);
assume r > inf seq ; :: thesis: contradiction
then r - (inf seq) > 0 by XREAL_1:52;
then ex k being Element of NAT st seq . k < (inf seq) + (r - (inf seq)) by A2, Th8;
hence contradiction by A1; :: thesis: verum

end;

hence r <= inf seq ; :: thesis: verum

end;

assume that
A3: seq is bounded_below and
A4: r <= inf seq ; :: thesis: for n being Element of NAT holds r <= seq . n

now

let n be Element of NAT ; :: thesis: r <= seq . n
inf seq <= seq . n by A3, Th8;
hence r <= seq . n by A4, XXREAL_0:2; :: thesis: verum

end;

hence for n being Element of NAT holds r <= seq . n ; :: thesis: verum