theorem Th16: :: HEYTING1:16

DISJOINT_PAIRS {} = {[{},{}]}