consider F being Field such that
A1: ([#] F) /\ ([#] (Polynom-Ring F)) <> {} by Th14;
take F ; :: thesis: not F is polynomial_disjoint
thus not F is polynomial_disjoint by A1; :: thesis: verum