let x be Real; :: thesis: ( sgn x = - 1 implies x < 0 )
assume that
A1: sgn x = - 1 and
A2: x >= 0 ; :: thesis: contradiction
( 0 < x or x = 0 ) by A2;
hence contradiction by A1, Def2; :: thesis: verum