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

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