theorem Th12: :: HEYTING1:12

for A being set holds [{},{}] is Element of DISJOINT_PAIRS A