let A be set ; :: thesis: for b being Element of DISJOINT_PAIRS A
for B being Element of Fin () st b in B holds
ex c being Element of DISJOINT_PAIRS A st
( c c= b & c in mi B )

let b be Element of DISJOINT_PAIRS A; :: thesis: for B being Element of Fin () st b in B holds
ex c being Element of DISJOINT_PAIRS A st
( c c= b & c in mi B )

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

assume A1: b in B ; :: thesis: ex c being Element of DISJOINT_PAIRS A st
( c c= b & c in mi B )

defpred S1[ Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A] means \$1 c= \$2;
A2: for a being Element of DISJOINT_PAIRS A holds S1[a,a] ;
A3: for a, b, c being Element of DISJOINT_PAIRS A st S1[a,b] & S1[b,c] holds
S1[a,c] by Th2;
for a being Element of DISJOINT_PAIRS A st a in B holds
ex b being Element of DISJOINT_PAIRS A st
( b in B & S1[b,a] & ( for c being Element of DISJOINT_PAIRS A st c in B & S1[c,b] holds
S1[b,c] ) ) from then consider c being Element of DISJOINT_PAIRS A such that
A4: c in B and
A5: c c= b and
A6: for a being Element of DISJOINT_PAIRS A st a in B & a c= c holds
c c= a by A1;
take c ; :: thesis: ( c c= b & c in mi B )
thus c c= b by A5; :: thesis: c in mi B
now :: thesis: for b being Element of DISJOINT_PAIRS A st b in B & b c= c holds
b = c
let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in B & b c= c implies b = c )
assume that
A7: b in B and
A8: b c= c ; :: thesis: b = c
c c= b by A6, A7, A8;
hence b = c by ; :: thesis: verum
end;
hence c in mi B by ; :: thesis: verum