let r, s be Real; :: thesis: ( r >= 0 & s > 0 implies r + s > 0 )
assume r >= 0 ; :: thesis: ( not s > 0 or r + s > 0 )
then r + s >= 0 + s by Lm5;
hence ( not s > 0 or r + s > 0 ) by Lm6; :: thesis: verum