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;

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

hence
mi (B ^ C) c= (mi B) ^ C
by Lm5; :: thesis: veruma 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;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