reconsider a = {} as set ;
consider m being ManySortedSet of ;
consider c being BinComp of m;
take AltCatStr(# a,m,c #) ; :: thesis: the carrier of AltCatStr(# a,m,c #) is empty
thus the carrier of AltCatStr(# a,m,c #) is empty ; :: thesis: verum