:: deftheorem defines ^- REALALG3:def 6 :
for R being Ring
for S being Subset of R holds S ^- = (- S) \ {(0. R)};