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