for X being set
for S being Subset of (id X) holds proj1 S = proj2 S