now :: thesis: not 2. R = 0. R

assume 2. R = 0. R ; :: thesis: contradiction
then 0. R = 2 '*' (1. R) by RING_5:2;
then Char R = 2 by REALALG2:24;
hence contradiction by RING_3:def 6; :: thesis: verum

end;

hence not 2. R is zero ; :: thesis: verum