let A be set ; :: thesis: for B, C being Element of Fin () holds mi ((mi B) \/ C) = mi (B \/ C)
let B, C be Element of Fin (); :: thesis: mi ((mi B) \/ C) = mi (B \/ C)
A1: (mi B) \/ C c= B \/ C by ;
now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi ((mi B) \/ C) holds
a in mi (B \/ C)
let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in mi ((mi B) \/ C) implies a in mi (B \/ C) )
assume A2: a in mi ((mi B) \/ C) ; :: thesis: a in mi (B \/ C)
A3: now :: thesis: for b being Element of DISJOINT_PAIRS A st b in B \/ C & b c= a holds
b = a
let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in B \/ C & b c= a implies b = a )
assume that
A4: b in B \/ C and
A5: b c= a ; :: thesis: b = a
now :: thesis: b = a
per cases ( b in B or b in C ) by ;
suppose b in B ; :: thesis: b = a
then consider c being Element of DISJOINT_PAIRS A such that
A6: c c= b and
A7: c in mi B by Th41;
( c in (mi B) \/ C & c c= a ) by ;
then c = a by ;
hence b = a by A5, A6, Th1; :: thesis: verum
end;
end;
end;
hence b = a ; :: thesis: verum
end;
a in (mi B) \/ C by ;
hence a in mi (B \/ C) by A1, A3, Th39; :: 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)
A8: mi (B \/ C) c= (mi B) \/ C by Th43;
now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi (B \/ C) holds
a in mi ((mi B) \/ C)
let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in mi (B \/ C) implies a in mi ((mi B) \/ C) )
assume A9: 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 ;
hence a in mi ((mi B) \/ C) by A8, A9, Th39; :: thesis: verum
end;
hence mi (B \/ C) c= mi ((mi B) \/ C) by Lm5; :: thesis: verum