theorem Th6: :: HEYTING1:6

for A being set
for a, c being Element of DISJOINT_PAIRS A st c in (Atom A) . a holds
c = a