( a >= 2 & x >= 1 ) by NAT_1:14, NAT_2:29;
then a * x >= 2 * 1 by XREAL_1:66;
then a * x <> 1 ;
hence not a * x is trivial by NAT_2:28; :: thesis: verum