thus ( seq is bounded_below implies ex r being Real st
for n being Nat holds r < seq . n ) :: thesis: ( ex r being Real st
for n being Nat holds r < seq . n implies seq is bounded_below )

proof

given r being Real such that A4: for y being object st y in dom seq holds
r < seq . y ; :: according to SEQ_2:def 2 :: thesis: ex r being Real st
for n being Nat holds r < seq . n
take r ; :: thesis: for n being Nat holds r < seq . n
let n be Nat; :: thesis: r < seq . n
n in NAT by ORDINAL1:def 12;
hence r < seq . n by A1, A4; :: thesis: verum

end;

given r being Real such that A5: for n being Nat holds r < seq . n ; :: thesis: seq is bounded_below
take r ; :: according to SEQ_2:def 2 :: thesis: for y being object st y in dom seq holds
r < seq . y
let y be object ; :: thesis: ( y in dom seq implies r < seq . y )
assume y in dom seq ; :: thesis: r < seq . y
hence r < seq . y by A5; :: thesis: verum