:: deftheorem defines carr FIELD_3:def 4 :
for R being non almost_trivial Ring
for x being non trivial Element of R
for o being object holds carr (x,o) = (([#] R) \ {x}) \/ {o};