per cases ( a is weightless or a is light ) by Th1;
suppose a is weightless ; :: thesis: not a |^ n is heavy
hence not a |^ n is heavy ; :: thesis: verum
end;
suppose a is light ; :: thesis: not a |^ n is heavy
then ( a |^ n is light or n = 0 ) ;
then ( a |^ n is light or a |^ n = 1 ) by NEWTON:4;
hence not a |^ n is heavy ; :: thesis: verum
end;
end;