theorem :: PARTIT_2:18

for X being non empty set holds field (id X) = X