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