take 1. (Polynom-Ring R) ; :: thesis: not 1. (Polynom-Ring R) is zero
thus not 1. (Polynom-Ring R) is zero ; :: thesis: verum