theorem Th1: :: WAYBEL20:1

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