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

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