dom (SymCl R) = (dom R) \/ (dom (R ~)) by XTUPLE_0:23
.= X \/ (dom (R ~)) by PARTFUN1:def 2
.= X by XBOOLE_1:12 ;
hence SymCl R is total by PARTFUN1:def 2; :: thesis: verum