theorem Th85: :: RING_3:86

for R being domRing holds
( Char R = 0 or Char R is prime )