let a, b be real number ; :: thesis: ( a > 0 implies a #R b >= 0 )
consider s being Rational_Sequence such that
A1: s is convergent and
A2: b = lim s and
for n being Element of NAT holds s . n <= b by Th79;
assume A3: a > 0 ; :: thesis: a #R b >= 0

A4: now

let n be Element of NAT ; :: thesis: (a #Q s) . n >= 0
(a #Q s) . n = a #Q (s . n) by Def7;
hence (a #Q s) . n >= 0 by A3, Th63; :: thesis: verum

end;

a #Q s is convergent by A3, A1, Th82;
then a #R b = lim (a #Q s) by A3, A1, A2, Def8;
hence a #R b >= 0 by A3, A1, A4, Th82, SEQ_2:17; :: thesis: verum