theorem Th67: :: FUNCT_7:68

for R being Relation holds iter (R,0) = id (field R)