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:49; :: thesis: verum