let x, y be ExtReal; :: thesis: ( x >= 0 & y > 0 implies x + y > 0 )
assume x >= 0 ; :: thesis: ( not y > 0 or x + y > 0 )
then x + y >= 0 + y by Lm12;
hence ( not y > 0 or x + y > 0 ) by Th4; :: thesis: verum