per cases ( [/a\] = [\a/] or [/a\] = [\a/] + 1 ) by INT_1:41;

suppose [/a\] = [\a/] ; :: thesis: [/a\] is weightless

hence [/a\] is weightless ; :: thesis: verum

end;

suppose B1: [/a\] = [\a/] + 1 ; :: thesis: [/a\] is weightless

then B2: [/a\] <> [\a/] ;
B3: a <= 1 by Th2;
[\a/] < a by B2, INT_1:26, INT_1:34;
then ( ( [\a/] is weightless & [\a/] is negative ) or [\a/] is zero ) by B3, TA1;
hence [/a\] is weightless by B1; :: thesis: verum

end;

end;