consider F being Field such that
A: ([#] F) /\ ([#] (Polynom-Ring F)) <> {} by FIELD_3:14;
reconsider K = F as non polynomial_disjoint Field by A, FIELD_3:def 3;
not K is strong_polynomial_disjoint ;
hence not for b₁ being Field holds b₁ is strong_polynomial_disjoint ; :: thesis: verum