theorem Th17: :: COMPUT_1:18
arity {} = 0