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 Th40, XBOOLE_1:9;

A8: mi (B \/ C) c= (mi B) \/ C by Th43;

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 Th40, XBOOLE_1:9;

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi ((mi B) \/ C) holds

a in mi (B \/ C)

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)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)

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

end;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

a in (mi B) \/ C
by A2, Th36;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

end;assume that

A4: b in B \/ C and

A5: b c= a ; :: thesis: b = a

now :: thesis: b = aend;

hence
b = a
; :: thesis: verumper cases
( b in B or b in C )
by A4, XBOOLE_0:def 3;

end;

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

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)

hence
mi (B \/ C) c= mi ((mi B) \/ C)
by Lm5; :: thesis: veruma 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 A1, Th36;

hence a in mi ((mi B) \/ C) by A8, A9, Th39; :: thesis: verum

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

hence a in mi ((mi B) \/ C) by A8, A9, Th39; :: thesis: verum