:: deftheorem Def4 defines Atom HEYTING1:def 4 :
for A being set
for b₂ being Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) holds
( b₂ = Atom A iff for a being Element of DISJOINT_PAIRS A holds b₂ . a = {a} );