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