set o = the set ;
take CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) ; :: thesis: ( not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty )
thus ( not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty ) ; :: thesis: verum