let A be set ; :: thesis: [{},{}] is Element of DISJOINT_PAIRS A
( [{},{}] = [({}. A),({}. A)] & [{},{}] `1 misses [{},{}] `2 ) ;
hence [{},{}] is Element of DISJOINT_PAIRS A by NORMFORM:29; :: thesis: verum