let A be set ; :: thesis: for K, L being Element of Normal_forms_on A holds mi ((K ^ L) \/ L) = mi L

let K, L be Element of Normal_forms_on A; :: thesis: mi ((K ^ L) \/ L) = mi L

let K, L be Element of Normal_forms_on A; :: thesis: mi ((K ^ L) \/ L) = mi L

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi ((K ^ L) \/ L) holds

a in mi L

hence
mi ((K ^ L) \/ L) c= mi L
by Lm5; :: according to XBOOLE_0:def 10 :: thesis: mi L c= mi ((K ^ L) \/ L)a in mi L

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in mi ((K ^ L) \/ L) implies a in mi L )

assume A1: a in mi ((K ^ L) \/ L) ; :: thesis: a in mi L

then ( a in K ^ L or a in L ) by XBOOLE_0:def 3;

hence a in mi L by A3, A2, Th39; :: thesis: verum

end;assume A1: a in mi ((K ^ L) \/ L) ; :: thesis: a in mi L

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

b = a

b = a

let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in L & b c= a implies b = a )

assume b in L ; :: thesis: ( b c= a implies b = a )

then b in (K ^ L) \/ L by XBOOLE_0:def 3;

hence ( b c= a implies b = a ) by A1, Th36; :: thesis: verum

end;assume b in L ; :: thesis: ( b c= a implies b = a )

then b in (K ^ L) \/ L by XBOOLE_0:def 3;

hence ( b c= a implies b = a ) by A1, Th36; :: thesis: verum

A3: now :: thesis: ( a in K ^ L implies a in L )

a in (K ^ L) \/ L
by A1, Th36;assume
a in K ^ L
; :: thesis: a in L

then consider b being Element of DISJOINT_PAIRS A such that

A4: b in L and

A5: b c= a by Lm7;

b in (K ^ L) \/ L by A4, XBOOLE_0:def 3;

hence a in L by A1, A4, A5, Th36; :: thesis: verum

end;then consider b being Element of DISJOINT_PAIRS A such that

A4: b in L and

A5: b c= a by Lm7;

b in (K ^ L) \/ L by A4, XBOOLE_0:def 3;

hence a in L by A1, A4, A5, Th36; :: thesis: verum

then ( a in K ^ L or a in L ) by XBOOLE_0:def 3;

hence a in mi L by A3, A2, Th39; :: thesis: verum

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi L holds

a in mi ((K ^ L) \/ L)

hence
mi L c= mi ((K ^ L) \/ L)
by Lm5; :: thesis: veruma in mi ((K ^ L) \/ L)

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in mi L implies a in mi ((K ^ L) \/ L) )

assume A6: a in mi L ; :: thesis: a in mi ((K ^ L) \/ L)

then A7: a in L by Th36;

hence a in mi ((K ^ L) \/ L) by A8, Th39; :: thesis: verum

end;assume A6: a in mi L ; :: thesis: a in mi ((K ^ L) \/ L)

then A7: a in L by Th36;

A8: now :: thesis: for b being Element of DISJOINT_PAIRS A st b in (K ^ L) \/ L & b c= a holds

b = a

a in (K ^ L) \/ L
by A7, XBOOLE_0:def 3;b = a

let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in (K ^ L) \/ L & b c= a implies b = a )

assume b in (K ^ L) \/ L ; :: thesis: ( b c= a implies b = a )

then A9: ( b in K ^ L or b in L ) by XBOOLE_0:def 3;

assume A10: b c= a ; :: thesis: b = a

end;assume b in (K ^ L) \/ L ; :: thesis: ( b c= a implies b = a )

then A9: ( b in K ^ L or b in L ) by XBOOLE_0:def 3;

assume A10: b c= a ; :: thesis: b = a

now :: thesis: ( b in K ^ L implies b in L )

hence
b = a
by A6, A9, A10, Th36; :: thesis: verumassume
b in K ^ L
; :: thesis: b in L

then consider c being Element of DISJOINT_PAIRS A such that

A11: c in L and

A12: c c= b by Lm7;

c c= a by A10, A12, Th2;

then c = a by A6, A11, Th36;

hence b in L by A7, A10, A12, Th1; :: thesis: verum

end;then consider c being Element of DISJOINT_PAIRS A such that

A11: c in L and

A12: c c= b by Lm7;

c c= a by A10, A12, Th2;

then c = a by A6, A11, Th36;

hence b in L by A7, A10, A12, Th1; :: thesis: verum

hence a in mi ((K ^ L) \/ L) by A8, Th39; :: thesis: verum