set a = the Element of DISJOINT_PAIRS A;
{ the Element of DISJOINT_PAIRS 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