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

proof

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

end;

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