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_{1}[ 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_{1}[a,a]
;

A3: for a, b, c being Element of DISJOINT_PAIRS A st S_{1}[a,b] & S_{1}[b,c] holds

S_{1}[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_{1}[b,a] & ( for c being Element of DISJOINT_PAIRS A st c in B & S_{1}[c,b] holds

S_{1}[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

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

A2: for a being Element of DISJOINT_PAIRS A holds S

A3: for a, b, c being Element of DISJOINT_PAIRS A st S

S

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

S

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

hence
c in mi B
by A4, Th39; :: thesis: verumb = 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;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