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