per cases ( a is zero or not a is zero ) ;

suppose a is zero ; :: thesis: [\a/] is zero

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

end;

suppose not a is zero ; :: thesis: [\a/] is zero

then reconsider a = a as positive light Real ;
( 0 <= a & a < [\0/] + 1 ) by TA1;
hence [\a/] is zero by INT_1:67; :: thesis: verum

end;

end;