let X be non empty set ; :: thesis: for R being total Relation of X holds field R = X
let R be total Relation of X; :: thesis: field R = X
field R = X \/ (rng R) by PARTFUN1:def 2;
hence field R = X by XBOOLE_1:12; :: thesis: verum