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;