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