theorem Th9: :: HEYTING3:9
for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)