( x = 0 or x > 0 or x < 0 ) ;
hence sgn x is integer by Def2; :: thesis: verum