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