theorem :: SUBSTLAT:25

for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K