theorem Th85: :: RING_3:86
for R being domRing holds
( Char R = 0 or Char R is prime )