for A being set
for a being Element of DISJOINT_PAIRS A
for u being Element of (NormForm A) st (@ u) ^ {a} = {} holds
(Atom A) . a [= (pseudo_compl A) . u