theorem Th15: :: HEYTING1:15

for a being Element of DISJOINT_PAIRS {} holds a = [{},{}]