:: deftheorem Def8 defines Atom HEYTING2:def 8 :
for V being set
for C being finite set
for b₃ being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) holds
( b₃ = Atom (V,C) iff for a being Element of PFuncs (V,C) holds b₃ . a = mi {.a.} );