for X being set
for x being object st x in X holds
(id X) . x = x by Th17;