let A be set ; :: thesis: for b, c being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds
b \/ c in B ^ C
let b, c be Element of DISJOINT_PAIRS A; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds
b \/ c in B ^ C
let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: ( b in B & c in C & b \/ c in DISJOINT_PAIRS A implies b \/ c in B ^ C )
assume ( b in B & c in C ) ; :: thesis: ( not b \/ c in DISJOINT_PAIRS A or b \/ c in B ^ C )
then A1: b \/ c in { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;
assume b \/ c in DISJOINT_PAIRS A ; :: thesis: b \/ c in B ^ C
hence b \/ c in B ^ C by A1, XBOOLE_0:def 4; :: thesis: verum