for A being set
for a being Element of DISJOINT_PAIRS A
for K being Element of Normal_forms_on A st K ^ {a} = {} holds
ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )