let A be set ; :: thesis: for a, b being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds

( a in B & ( b in B & b c= a implies b = a ) )

let a, b be Element of DISJOINT_PAIRS A; :: thesis: for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds

( a in B & ( b in B & b c= a implies b = a ) )

let B be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( a in mi B implies ( a in B & ( b in B & b c= a implies b = a ) ) )

assume a in mi B ; :: thesis: ( a in B & ( b in B & b c= a implies b = a ) )

then ex t being Element of DISJOINT_PAIRS A st

( a = t & ( for s being Element of DISJOINT_PAIRS A holds

( ( s in B & s c= t ) iff s = t ) ) ) ;

hence ( a in B & ( b in B & b c= a implies b = a ) ) ; :: thesis: verum

for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds

( a in B & ( b in B & b c= a implies b = a ) )

let a, b be Element of DISJOINT_PAIRS A; :: thesis: for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds

( a in B & ( b in B & b c= a implies b = a ) )

let B be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( a in mi B implies ( a in B & ( b in B & b c= a implies b = a ) ) )

assume a in mi B ; :: thesis: ( a in B & ( b in B & b c= a implies b = a ) )

then ex t being Element of DISJOINT_PAIRS A st

( a = t & ( for s being Element of DISJOINT_PAIRS A holds

( ( s in B & s c= t ) iff s = t ) ) ) ;

hence ( a in B & ( b in B & b c= a implies b = a ) ) ; :: thesis: verum