let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A

for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds

ex c being Element of DISJOINT_PAIRS A st

( c in C & c c= a )

let a be Element of DISJOINT_PAIRS A; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds

ex c being Element of DISJOINT_PAIRS A st

( c in C & c c= a )

let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( a in B ^ C implies ex c being Element of DISJOINT_PAIRS A st

( c in C & c c= a ) )

assume a in B ^ C ; :: thesis: ex c being Element of DISJOINT_PAIRS A st

( c in C & c c= a )

then consider b, c being Element of DISJOINT_PAIRS A such that

b in B and

A1: c in C and

A2: a = b \/ c by Th34;

take c ; :: thesis: ( c in C & c c= a )

thus c in C by A1; :: thesis: c c= a

thus c c= a by A2, Th10; :: thesis: verum

for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds

ex c being Element of DISJOINT_PAIRS A st

( c in C & c c= a )

let a be Element of DISJOINT_PAIRS A; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds

ex c being Element of DISJOINT_PAIRS A st

( c in C & c c= a )

let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( a in B ^ C implies ex c being Element of DISJOINT_PAIRS A st

( c in C & c c= a ) )

assume a in B ^ C ; :: thesis: ex c being Element of DISJOINT_PAIRS A st

( c in C & c c= a )

then consider b, c being Element of DISJOINT_PAIRS A such that

b in B and

A1: c in C and

A2: a = b \/ c by Th34;

take c ; :: thesis: ( c in C & c c= a )

thus c in C by A1; :: thesis: c c= a

thus c c= a by A2, Th10; :: thesis: verum