theorem Th79: :: RING_3:80
for R being Ring holds Char R = min* (CharSet R)