theorem T9: :: RING_4:19

for R being Ring
for a, b being Element of R holds
( a | R = b | R iff a = b )