let A be set ; :: thesis: for b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) 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 (DISJOINT_PAIRS A) 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 (DISJOINT_PAIRS A); :: 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 S₁[ Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A] means $1 c= $2;
A2: for a being Element of DISJOINT_PAIRS A holds S₁[a,a] ;
A3: for a, b, c being Element of DISJOINT_PAIRS A st S₁[a,b] & S₁[b,c] holds
S₁[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 & S₁[b,a] & ( for c being Element of DISJOINT_PAIRS A st c in B & S₁[c,b] holds
S₁[b,c] ) ) from FRAENKEL:sch 23(A2, A3);
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 A8, Th1; :: thesis: verum

end;

hence c in mi B by A4, Th39; :: thesis: verum