thus Fin (DISJOINT_PAIRS {}) = bool (DISJOINT_PAIRS {}) by Th16, FINSUB_1:14
.= {{},{[{},{}]}} by Th16, ZFMISC_1:24 ; :: thesis: verum