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

proof

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

end;

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