let a, b be Real; :: thesis: ( a >= 1 & b >= 0 implies a #R b >= 1 )
assume that
A1: a >= 1 and
A2: b >= 0 ; :: thesis: a #R b >= 1
consider s being Rational_Sequence such that
A3: s is convergent and
A4: b = lim s and
A5: for n being Nat holds s . n >= b by Th68;

A6: now :: thesis: for n being Nat holds (a #Q s) . n >= 1

let n be Nat; :: thesis: (a #Q s) . n >= 1
A7: (a #Q s) . n = a #Q (s . n) by Def5;
s . n >= b by A5;
hence (a #Q s) . n >= 1 by A1, A2, A7, Th60; :: thesis: verum

end;

a #Q s is convergent by A1, A3, Th69;
then a #R b = lim (a #Q s) by A1, A3, A4, Def6;
hence a #R b >= 1 by A1, A3, A6, Th1, Th69; :: thesis: verum