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