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