set a = the Function of {},({x} *);
set r = the Function of {},{x};
reconsider S = ManySortedSign(# {x},{}, the Function of {},({x} *), the Function of {},{x} #) as void strict ManySortedSign ;
take S ; :: thesis: the carrier of S = {x}
thus the carrier of S = {x} ; :: thesis: verum