:: deftheorem defines /" PRELAMB:def 2 :
for s being non empty typealg
for x, y being type of s holds x /" y = the right_quotient of s . (x,y);