theorem Th11: :: SUBSTLAT:11

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