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