theorem Th77: :: RING_3:78

for R being Ring holds
( Char R = 0 iff CharSet R = {} )