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