:: deftheorem defines right PRELAMB:def 6 :
for s being non empty typealg
for IT being type of s holds
( IT is right iff ex x, y being type of s st IT = x /" y );