let a, b be Real; :: 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 Nat holds s . n <= b by Th67;

assume A3: a > 0 ; :: thesis: a #R b >= 0

then a #R b = lim (a #Q s) by A3, A1, A2, Def6;

hence a #R b >= 0 by A3, A1, A4, Th69, SEQ_2:17; :: thesis: verum

consider s being Rational_Sequence such that

A1: s is convergent and

A2: b = lim s and

for n being Nat holds s . n <= b by Th67;

assume A3: a > 0 ; :: thesis: a #R b >= 0

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

a #Q s is convergent
by A3, A1, Th69;let n be Nat; :: thesis: (a #Q s) . n >= 0

(a #Q s) . n = a #Q (s . n) by Def5;

hence (a #Q s) . n >= 0 by A3, Th52; :: thesis: verum

end;(a #Q s) . n = a #Q (s . n) by Def5;

hence (a #Q s) . n >= 0 by A3, Th52; :: thesis: verum

then a #R b = lim (a #Q s) by A3, A1, A2, Def6;

hence a #R b >= 0 by A3, A1, A4, Th69, SEQ_2:17; :: thesis: verum