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

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