set o = the set ;
take ProdCatStr(# { 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 ProdCatStr(# { 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 ProdCatStr(# { 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 ProdCatStr(# { 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 ProdCatStr(# { 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