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 b being Element of DISJOINT_PAIRS A st

( b c= a & b in (mi B) ^ C )

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 b being Element of DISJOINT_PAIRS A st

( b c= a & b in (mi B) ^ C )

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

( b c= a & b in (mi B) ^ C ) )

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

( b c= a & b in (mi B) ^ C )

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

A1: b in B and

A2: c in C and

A3: a = b \/ c by Th34;

consider d being Element of DISJOINT_PAIRS A such that

A4: d c= b and

A5: d in mi B by A1, Th41;

d \/ c c= a by A3, A4, Th12;

then reconsider e = d \/ c as Element of DISJOINT_PAIRS A by Th26;

take e ; :: thesis: ( e c= a & e in (mi B) ^ C )

thus e c= a by A3, A4, Th12; :: thesis: e in (mi B) ^ C

thus e in (mi B) ^ C by A2, A5, Th35; :: thesis: verum

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

ex b being Element of DISJOINT_PAIRS A st

( b c= a & b in (mi B) ^ C )

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 b being Element of DISJOINT_PAIRS A st

( b c= a & b in (mi B) ^ C )

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

( b c= a & b in (mi B) ^ C ) )

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

( b c= a & b in (mi B) ^ C )

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

A1: b in B and

A2: c in C and

A3: a = b \/ c by Th34;

consider d being Element of DISJOINT_PAIRS A such that

A4: d c= b and

A5: d in mi B by A1, Th41;

d \/ c c= a by A3, A4, Th12;

then reconsider e = d \/ c as Element of DISJOINT_PAIRS A by Th26;

take e ; :: thesis: ( e c= a & e in (mi B) ^ C )

thus e c= a by A3, A4, Th12; :: thesis: e in (mi B) ^ C

thus e in (mi B) ^ C by A2, A5, Th35; :: thesis: verum