let X be set ; :: thesis: for a being Element of DISJOINT_PAIRS X
for x being set holds
( not x in a `1 or not x in a `2 )
let a be Element of DISJOINT_PAIRS X; :: thesis: for x being set holds
( not x in a `1 or not x in a `2 )
a `1 misses a `2 by Th42;
hence for x being set holds
( not x in a `1 or not x in a `2 ) by XBOOLE_0:3; :: thesis: verum