:: deftheorem defines Mor CLASSES5:def 28 :
for C being quintuple StrCategory-like Category-like set holds Mor C = C `2 ;