let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds
b = a ) holds
a in mi B
let a be Element of DISJOINT_PAIRS A; :: thesis: for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds
b = a ) holds
a in mi B
let B be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds
b = a ) implies a in mi B )
assume ( a in B & ( for s being Element of DISJOINT_PAIRS A st s in B & s c= a holds
s = a ) ) ; :: thesis: a in mi B
then for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= a ) iff s = a ) ;
hence a in mi B ; :: thesis: verum