let X be set ; :: thesis: for y being Element of [:(Fin X),(Fin X):] holds
( y in DISJOINT_PAIRS X iff y `1 misses y `2 )
let y be Element of [:(Fin X),(Fin X):]; :: thesis: ( y in DISJOINT_PAIRS X iff y `1 misses y `2 )
( y in DISJOINT_PAIRS X iff ex a being Element of [:(Fin X),(Fin X):] st
( y = a & a `1 misses a `2 ) ) ;
hence ( y in DISJOINT_PAIRS X iff y `1 misses y `2 ) ; :: thesis: verum