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