for R being Relation
for X being set st R is reflexive & X c= field R holds
field (R |_2 X) = X by Lm7;