theorem FieldTot: :: PREFER_1:18

for X being non empty set
for R being total Relation of X holds field R = X