theorem Th48:
for
S being non
empty non
void 4,1
integer BoolSignature for
I being
integer SortSymbol of
S holds
(
I <> the
bool-sort of
S & the
connectives of
S . 4
is_of_type {} ,
I & the
connectives of
S . (4 + 1) is_of_type {} ,
I & the
connectives of
S . 4
<> the
connectives of
S . (4 + 1) & the
connectives of
S . (4 + 2) is_of_type <*I*>,
I & the
connectives of
S . (4 + 3) is_of_type <*I,I*>,
I & the
connectives of
S . (4 + 4) is_of_type <*I,I*>,
I & the
connectives of
S . (4 + 5) is_of_type <*I,I*>,
I & the
connectives of
S . (4 + 3) <> the
connectives of
S . (4 + 4) & the
connectives of
S . (4 + 3) <> the
connectives of
S . (4 + 5) & the
connectives of
S . (4 + 4) <> the
connectives of
S . (4 + 5) & the
connectives of
S . (4 + 6) is_of_type <*I,I*>, the
bool-sort of
S )