set R = SymmetricHull W;
the carrier of W c= dom (SymmetricHull W)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in the carrier of W or t in dom (SymmetricHull W) )
assume t in the carrier of W ; :: thesis: t in dom (SymmetricHull W)
then reconsider tt = t as Element of W ;
tt <= tt ;
then [tt,tt] in SymmetricHull W by SymHull;
hence t in dom (SymmetricHull W) by XTUPLE_0:def 12; :: thesis: verum

end;

then dom (SymmetricHull W) = the carrier of W by XBOOLE_0:def 10;
hence SymmetricHull W is total by PARTFUN1:def 2; :: thesis: verum