reconsider X = the empty set as set ;
reconsider F = the PartFunc of [: the empty set , the empty set :], the empty set as PartFunc of [:X,X:],X ;
set C = CategoryStr(# X,F #);
take CategoryStr(# X,F #) ; :: thesis: CategoryStr(# X,F #) is empty
thus CategoryStr(# X,F #) is empty ; :: thesis: verum