:: deftheorem Def20 defines quotient QUOFIELD:def 24 :
for I being non empty ZeroStr
for x, y being Element of I st y <> 0. I holds
quotient (x,y) = [x,y];