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