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

let B, C be Element of Fin (DISJOINT_PAIRS A); :: 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

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 A1: a in mi (B \/ C) ; :: thesis: a in (mi B) \/ C

then A2: a in B \/ C by Th36;

end;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) \/ Cend;

hence
a in (mi B) \/ C
; :: thesis: verumper cases
( a in B or a in C )
by A2, XBOOLE_0:def 3;

end;

suppose A3:
a in B
; :: thesis: a in (mi B) \/ C

hence a in (mi B) \/ C by XBOOLE_0:def 3; :: thesis: verum

end;

now :: thesis: for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds

b = a

then
a in mi B
by A3, Th39;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 A1, Th36; :: thesis: verum

end;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 A1, Th36; :: thesis: verum

hence a in (mi B) \/ C by XBOOLE_0:def 3; :: thesis: verum