theorem :: HEYTING1:8

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