let r be Real; :: thesis: for seq being Real_Sequence holds
( ( for n being Nat holds r <= seq . n ) iff ( seq is bounded_below & r <= lower_bound seq ) )
let seq be Real_Sequence; :: thesis: ( ( for n being Nat holds r <= seq . n ) iff ( seq is bounded_below & r <= lower_bound seq ) )
thus ( ( for n being Nat holds r <= seq . n ) implies ( seq is bounded_below & r <= lower_bound seq ) ) :: thesis: ( seq is bounded_below & r <= lower_bound seq implies for n being Nat holds r <= seq . n )

proof

assume A1: for n being Nat holds r <= seq . n ; :: thesis: ( seq is bounded_below & r <= lower_bound seq )

now :: thesis: for m being Nat holds r - 1 < seq . m

let m be 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 <= lower_bound seq

now :: thesis: not r > lower_bound seq

set r1 = r - (lower_bound seq);
assume r > lower_bound seq ; :: thesis: contradiction
then r - (lower_bound seq) > 0 by XREAL_1:50;
then ex k being Nat st seq . k < (lower_bound seq) + (r - (lower_bound seq)) by A2, Th8;
hence contradiction by A1; :: thesis: verum

end;

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

end;

assume that
A3: seq is bounded_below and
A4: r <= lower_bound seq ; :: thesis: for n being Nat holds r <= seq . n

now :: thesis: for n being Nat holds r <= seq . n

let n be Nat; :: thesis: r <= seq . n
lower_bound seq <= seq . n by A3, Th8;
hence r <= seq . n by A4, XXREAL_0:2; :: thesis: verum

end;

hence for n being Nat holds r <= seq . n ; :: thesis: verum