consider o, m being set ;
take ProdCatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m),(Extract o),(o,o :-> o),(o,o :-> m),(o,o :-> m) #) ; :: thesis: ( not ProdCatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m),(Extract o),(o,o :-> o),(o,o :-> m),(o,o :-> m) #) is void & not ProdCatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m),(Extract o),(o,o :-> o),(o,o :-> m),(o,o :-> m) #) is empty )
thus ( not ProdCatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m),(Extract o),(o,o :-> o),(o,o :-> m),(o,o :-> m) #) is void & not ProdCatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m),(Extract o),(o,o :-> o),(o,o :-> m),(o,o :-> m) #) is empty ) ; :: thesis: verum