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