take 0_. R ; :: thesis: not 0_. R is linear
thus not 0_. R is linear by HURWITZ:20; :: thesis: verum