set o = {} ;
set m = {} ;
set C = 1Cat ({},{});
A1: 1Cat ({},{}) = CatStr(# {{}},{{}},({} :-> {}),({} :-> {}),(({},{}) :-> {}) #) by CAT_1:def 11;
reconsider y1 = {{}} as set ;
reconsider y2 = {{}} as set ;
reconsider y3 = {} :-> {} as Function of y2,y1 ;
reconsider y4 = {} :-> {} as Function of y2,y1 ;
reconsider y5 = ({},{}) :-> {} as Function of [:y2,y2:],y2 ;
reconsider CC = [y1,y2,y3,y4,y5] as quintuple set ;
CC is StrCategory-like ;
then reconsider CC = CC as quintuple StrCategory-like set ;
take CC ; :: thesis: CC is Category-like
thus CC is Category-like by A1; :: thesis: verum