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