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