Theorem I. (a) In whatever way the symbol “Tr”, denoting a class of expressions, is defined in LGTC+, it will be possible to derive from it the negation of one of the sentences which were described in the condition (a) of the convention T;