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