set CC = CatToSet C;
reconsider CC = CatToSet C as quintuple set ;
reconsider y1 = the carrier of C as non empty set ;
reconsider y2 = the carrier' of C as set ;
reconsider y3 = the Source of C as Function of y2,y1 ;
reconsider y4 = the Target of C as Function of y2,y1 ;
reconsider y5 = the Comp of C as PartFunc of [:y2,y2:],y2 ;
CC is StrCategory-like ;
then reconsider CC = CC as quintuple StrCategory-like set ;
reconsider CC9 = CatStr(# y1,y2,y3,y4,y5 #) as CatStr ;
A1: ex y1, y2, y3, y4, y5 being set st
( y1 = CC `1 & y2 = CC `2 & y3 = CC `3 & y4 = CC `4 & y5 = CC `5 & y3 is Function of y2,y1 & y4 is Function of y2,y1 & y5 is PartFunc of [:y2,y2:],y2 ) ;
reconsider CC = CC as quintuple StrCategory-like Category-like set by Def27, A1;
CC is non-empty ;
hence CatToSet C is CategorySet ; :: thesis: verum