let A be set ; :: thesis: for K being Element of Normal_forms_on A holds mi (K ^ K) = mi K
let K be Element of Normal_forms_on A; :: thesis: mi (K ^ K) = mi K
thus mi (K ^ K) = mi ((K ^ K) \/ K) by Th54, XBOOLE_1:12
.= mi K by Lm8 ; :: thesis: verum