let a, b be real number ; :: thesis: ( a >= 1 & b >= 0 implies a #R b >= 1 )
assume A1: ( a >= 1 & b >= 0 ) ; :: thesis: a #R b >= 1
consider s being Rational_Sequence such that
A2: ( s is convergent & b = lim s & ( for n being Element of NAT holds s . n >= b ) ) by Th80;
A3: a #Q s is convergent by A1, A2, Th82;
then A4: a #R b = lim (a #Q s) by A1, A2, Def8;

now

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

end;

hence a #R b >= 1 by A3, A4, Th2; :: thesis: verum