theorem :: RINFSUP1:27

for k being Nat
for seq being Real_Sequence st seq is bounded_below holds
seq ^\ k is bounded_below by SEQM_3:28;