let A be set ; :: thesis: for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds
a = b
let a, b be Element of DISJOINT_PAIRS A; :: thesis: for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds
a = b
let B be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( B in Normal_forms_on A & a in B & b in B & a c= b implies a = b )
assume B in Normal_forms_on A ; :: thesis: ( not a in B or not b in B or not a c= b or a = b )
then ex C being Element of Fin (DISJOINT_PAIRS A) st
( B = C & ( for a, b being Element of DISJOINT_PAIRS A st a in C & b in C & a c= b holds
a = b ) ) ;
hence ( not a in B or not b in B or not a c= b or a = b ) ; :: thesis: verum