:: deftheorem defines compsym CATALG_1:def 10 :
for a, b, c being set holds compsym (a,b,c) = [2,<*a,b,c*>];