{} is Element of Fin X by FINSUB_1:7;
then reconsider b = [{},{}] as Element of [:(Fin X),(Fin X):] by ZFMISC_1:def 2;
b `1 misses b `2 ;
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