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

let K be Element of Normal_forms_on A; :: thesis: mi (K ^ K) = K

thus mi (K ^ K) = mi K by NORMFORM:55

.= K by NORMFORM:42 ; :: thesis: verum

let K be Element of Normal_forms_on A; :: thesis: mi (K ^ K) = K

thus mi (K ^ K) = mi K by NORMFORM:55

.= K by NORMFORM:42 ; :: thesis: verum