:: deftheorem defines Der RINGDER1:def 2 :
for R being non degenerated comRing holds Der R = { f where f is Function of R,R : f is derivation } ;