:: deftheorem defines \ PRELAMB:def 1 :
for s being non empty typealg
for x, y being type of s holds x \ y = the left_quotient of s . (x,y);