let a be Real; :: thesis: ( a is weightless iff a = sgn a )
A1: ( a is weightless implies a = sgn a )

proof

assume a is weightless ; :: thesis: a = sgn a
then ( a = 0 or a = |.1.| or - a = |.1.| ) by ABSVALUE:1;
hence a = sgn a by ABSVALUE:def 2; :: thesis: verum

end;

( a = sgn a implies a is weightless )

proof

assume A1: a = sgn a ; :: thesis: a is weightless
( a > 0 or a = 0 or a < 0 ) ;
then ( sgn a = 0 or sgn a = 1 or sgn a = - 1 ) by ABSVALUE:def 2;
hence a is weightless by A1; :: thesis: verum

end;

hence ( a is weightless iff a = sgn a ) by A1; :: thesis: verum