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