theorem :: ABSVALUE:14

for x being Real st sgn x = 1 holds
0 < x