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