theorem Th22: :: HEYTING2:22

for V being set
for C being finite set
for u being Element of (SubstLatt (V,C))
for K, L being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u