for X being set
for R being total Relation of X holds field R = X by Lm4;