let a, b be real number ; :: 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 Element of NAT holds s . n >= b by Th80;

A6: now

let n be Element of NAT ; :: thesis: (a #Q s) . n >= 1
A7: (a #Q s) . n = a #Q (s . n) by Def7;
s . n >= b by A5;
hence (a #Q s) . n >= 1 by A1, A2, A7, Th71; :: thesis: verum

end;

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