theorem Th13: :: RELSET_1:13

for X being set holds id X c= [:X,X:]