let A be set ; :: thesis: for B, C being Element of Fin () holds mi (B \/ C) c= (mi B) \/ C
let B, C be Element of Fin (); :: thesis: mi (B \/ C) c= (mi B) \/ C
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 A1: a in mi (B \/ C) ; :: thesis: a in (mi B) \/ C
then A2: a in B \/ C by Th36;
now :: thesis: a in (mi B) \/ C
per cases ( a in B or a in C ) by ;
suppose A3: a in B ; :: thesis: a in (mi B) \/ C
now :: thesis: for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds
b = a
let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in B & b c= a implies b = a )
assume b in B ; :: thesis: ( b c= a implies b = a )
then b in B \/ C by XBOOLE_0:def 3;
hence ( b c= a implies b = a ) by ; :: thesis: verum
end;
then a in mi B by ;
hence a in (mi B) \/ C by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence a in (mi B) \/ C ; :: thesis: verum
end;
hence mi (B \/ C) c= (mi B) \/ C by Lm5; :: thesis: verum