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:9;
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