theorem Th1: :: SUBSTLAT:1

for V, C being set holds {} in SubstitutionSet (V,C)