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 ; :: 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 ;
hence a in L by A1, A4, A5, Th36; :: thesis: verum
end;
a in (K ^ L) \/ L by ;
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 ;
then c = a by ;
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 ;
hence a in mi ((K ^ L) \/ L) by ; :: thesis: verum
end;
hence mi L c= mi ((K ^ L) \/ L) by Lm5; :: thesis: verum