If x * y = 0 then x or y is 0 test

Prove:

integer(X) and any(X) and integer(Y) and any(Y) and X * Y = 0=> X = 0 or Y = 0

Given:

Axiom	Definition
zero_times	integer(X) and any(X) and true=> X * 0 = 0 ;
division	integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and true and true and true and X * Y = X * Z and not X = 0=> Y = Z ;