:: deftheorem defines id$ COH_SP:def 23 :
for X being set
for T being Element of TOL X holds id$ T = [[T,T],(id (T `2))];