take Z/ 2 ; :: thesis: Z/ 2 is polynomial_disjoint
not 2 is trivial by NAT_2:def 1;
hence Z/ 2 is polynomial_disjoint ; :: thesis: verum