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

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