thus ( seq is bounded_above implies ex r being real number st
for n being Element of NAT holds seq . n < r ) :: thesis: ( ex r being real number st
for n being Element of NAT holds seq . n < r implies seq is bounded_above )

proof

given r being real number such that A2: for y being set st y in dom seq holds
seq . y < r ; :: according to SEQ_2:def 1 :: thesis: ex r being real number st
for n being Element of NAT holds seq . n < r
take r ; :: thesis: for n being Element of NAT holds seq . n < r
let n be Element of NAT ; :: thesis: seq . n < r
thus seq . n < r by A1, A2; :: thesis: verum

end;

given r being real number such that A3: for n being Element of NAT holds seq . n < r ; :: thesis: seq is bounded_above
take r ; :: according to SEQ_2:def 1 :: thesis: for y being set st y in dom seq holds
seq . y < r
let y be set ; :: thesis: ( y in dom seq implies seq . y < r )
assume y in dom seq ; :: thesis: seq . y < r
hence seq . y < r by A1, A3; :: thesis: verum