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