let A be set ; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) \/ C) = mi (B \/ C)
let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: mi ((mi B) \/ C) = mi (B \/ C)
A1: (mi B) \/ C c= B \/ C by Th64, XBOOLE_1:9;
A2: mi (B \/ C) c= (mi B) \/ C by Th67;

now

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in mi ((mi B) \/ C) implies a in mi (B \/ C) )
assume A3: a in mi ((mi B) \/ C) ; :: thesis: a in mi (B \/ C)
then A4: a in (mi B) \/ C by Th58;

now

let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in B \/ C & b c= a implies b = a )
assume that
A5: b in B \/ C and
A6: b c= a ; :: thesis: b = a

now

per cases ( b in B or b in C ) by A5, XBOOLE_0:def 3;

suppose b in B ; :: thesis: b = a

then consider c being Element of DISJOINT_PAIRS A such that
A7: c c= b and
A8: c in mi B by Th65;
A9: c in (mi B) \/ C by A8, XBOOLE_0:def 3;
c c= a by A6, A7, Th5;
then c = a by A3, A9, Th58;
hence b = a by A6, A7, Th4; :: thesis: verum

end;

suppose b in C ; :: thesis: b = a

then b in (mi B) \/ C by XBOOLE_0:def 3;
hence b = a by A3, A6, Th58; :: thesis: verum

end;

end;

end;

hence b = a ; :: thesis: verum

end;

hence a in mi (B \/ C) by A1, A4, Th61; :: thesis: verum

end;

hence mi ((mi B) \/ C) c= mi (B \/ C) by Lm5; :: according to XBOOLE_0:def 10 :: thesis: mi (B \/ C) c= mi ((mi B) \/ C)

now

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in mi (B \/ C) implies a in mi ((mi B) \/ C) )
assume A10: a in mi (B \/ C) ; :: thesis: a in mi ((mi B) \/ C)
then for b being Element of DISJOINT_PAIRS A st b in (mi B) \/ C & b c= a holds
b = a by A1, Th58;
hence a in mi ((mi B) \/ C) by A2, A10, Th61; :: thesis: verum

end;

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