consider a being Element of DISJOINT_PAIRS A;
{a} is Element of Normal_forms_on A by Lm1;
hence not for b₁ being Element of Normal_forms_on A holds b₁ is empty ; :: thesis: verum