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