theorem Th13: :: AOFA_A01:13

for S being non empty non void bool-correct 4,1 integer BoolSignature
for o being OperSymbol of S st o = In (( the connectives of S . 3), the carrier' of S) holds
( o = the connectives of S . 3 & the_arity_of o = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of o = the bool-sort of S )