:: deftheorem defines Obj CLASSES5:def 27 :
for C being quintuple StrCategory-like Category-like set holds Obj C = C `1 ;