let A be set ; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ C) c= (mi B) ^ C
let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: mi (B ^ C) c= (mi B) ^ C
A1: (mi B) ^ C c= B ^ C by Th40, Th46;

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi (B ^ C) holds
a in (mi B) ^ C

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in mi (B ^ C) implies a in (mi B) ^ C )
assume A2: a in mi (B ^ C) ; :: thesis: a in (mi B) ^ C
then a in B ^ C by Th36;
then ex b being Element of DISJOINT_PAIRS A st
( b c= a & b in (mi B) ^ C ) by Lm6;
hence a in (mi B) ^ C by A1, A2, Th36; :: thesis: verum

end;

hence mi (B ^ C) c= (mi B) ^ C by Lm5; :: thesis: verum