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_{1} being Field holds b_{1} is strong_polynomial_disjoint
; :: thesis: verum

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