theorem :: REALALG2:24

for R being non degenerated Ring holds
( Char R = 2 iff 2 '*' (1. R) = 0. R ) by P5b;