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