let n be Integer; :: thesis: ( not n is weightless implies n is heavy )
assume not n is weightless ; :: thesis: n is heavy
then ( n <> 1 & n <> - 1 & ( n is positive or n is negative ) ) ;
then ( ( n >= 0 + 1 & n <> 1 ) or ( n <= - 1 & n <> - 1 ) ) by INT_1:7, INT_1:8;
then ( n < - 1 or n > 1 ) by XXREAL_0:1;
hence n is heavy by COMPLEX3:1; :: thesis: verum