let X be set ; :: thesis: for a being Element of DISJOINT_PAIRS X

for V, W being set st V c= a `1 & W c= a `2 holds

[V,W] is Element of DISJOINT_PAIRS X

let a be Element of DISJOINT_PAIRS X; :: thesis: for V, W being set st V c= a `1 & W c= a `2 holds

[V,W] is Element of DISJOINT_PAIRS X

let V, W be set ; :: thesis: ( V c= a `1 & W c= a `2 implies [V,W] is Element of DISJOINT_PAIRS X )

assume A1: ( V c= a `1 & W c= a `2 ) ; :: thesis: [V,W] is Element of DISJOINT_PAIRS X

then ( V is Element of Fin X & W is Element of Fin X ) by SETWISEO:11;

then reconsider x = [V,W] as Element of [:(Fin X),(Fin X):] by ZFMISC_1:def 2;

( a `1 misses a `2 & [V,W] `1 = V ) by Th23;

then x `1 misses x `2 by A1, XBOOLE_1:64;

hence [V,W] is Element of DISJOINT_PAIRS X by Th23; :: thesis: verum

for V, W being set st V c= a `1 & W c= a `2 holds

[V,W] is Element of DISJOINT_PAIRS X

let a be Element of DISJOINT_PAIRS X; :: thesis: for V, W being set st V c= a `1 & W c= a `2 holds

[V,W] is Element of DISJOINT_PAIRS X

let V, W be set ; :: thesis: ( V c= a `1 & W c= a `2 implies [V,W] is Element of DISJOINT_PAIRS X )

assume A1: ( V c= a `1 & W c= a `2 ) ; :: thesis: [V,W] is Element of DISJOINT_PAIRS X

then ( V is Element of Fin X & W is Element of Fin X ) by SETWISEO:11;

then reconsider x = [V,W] as Element of [:(Fin X),(Fin X):] by ZFMISC_1:def 2;

( a `1 misses a `2 & [V,W] `1 = V ) by Th23;

then x `1 misses x `2 by A1, XBOOLE_1:64;

hence [V,W] is Element of DISJOINT_PAIRS X by Th23; :: thesis: verum