let a be Element of R; :: thesis: ( not a is zero & not a is O -positive implies a is O -negative )
assume A: ( not a is zero & not a is O -positive ) ; :: thesis: a is O -negative
then ( a <> 0. R & not 0. R < O,a ) by x1;
then ( a < O, 0. R or a = 0. R ) by avb4;
hence a is O -negative by A, x2; :: thesis: verum