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