:: deftheorem defines Unit_Set RINGFRAC:def 5 :
for R being commutative Ring holds Unit_Set R = { a where a is Element of R : a is Unit of R } ;