let X be ManySortedSet of {} ; :: thesis: X = {}
dom X = {} by Def3;
hence X = {} by RELAT_1:64; :: thesis: verum