let r be ext-real number ; :: thesis: ( not r is negative & not r is zero implies r is positive )
assume ( r >= 0 & r <> 0 ) ; :: according to XXREAL_0:def 7,XXREAL_0:def 8 :: thesis: r is positive
hence r > 0 by Th1; :: according to XXREAL_0:def 6 :: thesis: verum