let X be non empty set ; :: thesis: for R being total reflexive Relation of X holds R ~ is total
let R be total reflexive Relation of X; :: thesis: R ~ is total
dom R = X by PARTFUN1:def 2;
then dom (R ~) = X by RELAT_2:12;
hence R ~ is total by PARTFUN1:def 2; :: thesis: verum