:: deftheorem defines left PRELAMB:def 5 :
for s being non empty typealg
for IT being type of s holds
( IT is left iff ex x, y being type of s st IT = x \ y );