:: deftheorem defines 2. REALALG3:def 1 :
for R being Ring holds 2. R = (1. R) + (1. R);