{} is Element of Fin X by FINSUB_1:18;
then reconsider b = [{} ,{} ] as Element of [:(Fin X),(Fin X):] by ZFMISC_1:def 2;
( b `1 = {} & b `2 = {} ) by MCART_1:7;
then b `1 misses b `2 by XBOOLE_1:65;
then b in { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;
hence not DISJOINT_PAIRS X is empty ; :: thesis: verum