theorem Th79: :: RING_3:80

for R being Ring holds Char R = min* (CharSet R)