theorem :: COH_SP:37

for X being set holds [(id X),X] in TOL X by Th34;