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