A: Char R = 2 by RING_3:def 6;
then not R is degenerated by REALALG2:23;
then 0. R = 2 '*' (1. R) by A, REALALG2:24
.= (1. R) + (1. R) by RING_5:2 ;
hence 2. R is zero ; :: thesis: verum