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