theorem :: RELAT_1:46

for X being set holds (id X) ~ = id X ;