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_{1} being Element of Normal_forms_on A holds b_{1} is empty
; :: thesis: verum

{ the Element of DISJOINT_PAIRS A} is Element of Normal_forms_on A by Lm1;

hence not for b