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

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi ((K ^ L) \/ L) holds
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

A2: now :: thesis: for b being Element of DISJOINT_PAIRS A st b in L & b c= a holds
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;

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

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;

a in (K ^ L) \/ L by A1, Th36;
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;

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

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in mi L holds
a 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;

A8: now :: thesis: for b being Element of DISJOINT_PAIRS A st b in (K ^ L) \/ L & b c= a holds
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

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

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

hence b = a by A6, A9, A10, Th36; :: thesis: verum

end;

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

end;

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