set Z = the carrier of S --> {0};
set Y = X (\/) ( the carrier of S --> {0});
t is Term of S,(X (\/) ( the carrier of S --> {0})) by MSAFREE3:8;
then rng t c= the carrier of (DTConMSA (X (\/) ( the carrier of S --> {0}))) by RELAT_1:def 19;
hence rng t is Relation-like ; :: thesis: verum