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

suppose a is zero ; :: thesis: ( a div (a * b) is weightless & not a div (a * b) is positive )

hence ( a div (a * b) is weightless & not a div (a * b) is positive ) ; :: thesis: verum

end;

suppose not a is zero ; :: thesis: ( a div (a * b) is weightless & not a div (a * b) is positive )

then reconsider a = a as non light Integer ;

per cases ( b is negative or b is positive ) ;

suppose b is negative ; :: thesis: ( a div (a * b) is weightless & not a div (a * b) is positive )

then reconsider b = b as negative heavy Real ;
[\(a / (a * b))/] is non positive weightless Real ;
hence ( a div (a * b) is weightless & not a div (a * b) is positive ) by INT_1:def 9; :: thesis: verum

end;

suppose b is positive ; :: thesis: ( a div (a * b) is weightless & not a div (a * b) is positive )

then reconsider b = b as positive heavy Real ;
[\(a / (a * b))/] is non positive weightless Real ;
hence ( a div (a * b) is weightless & not a div (a * b) is positive ) by INT_1:def 9; :: thesis: verum

end;

end;

end;

end;