:: deftheorem defines id$ COH_SP:def 9 :
for X being set
for C being Element of CSp X holds id$ C = [[C,C],(id (union C))];