theorem Th87: :: RING_3:88
for R being Ring
for S being b1 -monomorphic Ring holds Char S = Char R