theorem Th2: :: SUBSTLAT:2

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