:: deftheorem defines idsym CATALG_1:def 8 :
for a being set holds idsym a = [1,<*a*>];