take 0. R ; :: thesis: not 0. R is prime
thus not 0. R is prime ; :: thesis: verum