:: deftheorem Def27 defines Category-like CLASSES5:def 26 :
for C being quintuple StrCategory-like set holds
( C is Category-like iff ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & CatStr(# y1,y2,y3,y4,y5 #) is Category ) );