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;

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

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

a #Q s is convergent
by A1, A3, Th69;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;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

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