theorem Th21: :: FOMODEL0:21

for Y being set
for R being b₁ -defined total Relation holds id Y c= R * (R ~)