theorem Th7: :: HEYTING1:7

for A being set
for a being Element of DISJOINT_PAIRS A holds a in (Atom A) . a