theorem Th8: :: PARTIT_2:8

for R being Relation
for Y being set st R is_reflexive_in Y holds
Y c= field R