let A be set ; :: thesis: for B being Element of Fin (DISJOINT_PAIRS A) holds mi B c= B
let B be Element of Fin (DISJOINT_PAIRS A); :: thesis: mi B c= B
for a being Element of DISJOINT_PAIRS A st a in mi B holds
a in B by Th36;
hence mi B c= B by Lm5; :: thesis: verum