theorem Th1: :: FUNCT_5:1

~ {} = {}