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