let V, C be set ; :: thesis: for K being Element of SubstitutionSet V,C holds mi (K ^ K) = K
let K be Element of SubstitutionSet V,C; :: thesis: mi (K ^ K) = K
thus mi (K ^ K) = mi K by Th24
.= K by Th11 ; :: thesis: verum