consider X being non empty set , A being ManySortedSet of , C being BinComp of A;
take AltCatStr(# X,A,C #) ; :: thesis: ( AltCatStr(# X,A,C #) is strict & not AltCatStr(# X,A,C #) is empty )
thus AltCatStr(# X,A,C #) is strict ; :: thesis: not AltCatStr(# X,A,C #) is empty
thus not the carrier of AltCatStr(# X,A,C #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum