theorem Th3: :: MSAFREE2:3

for G being non empty ManySortedSign holds SortsWithConstants G c= InnerVertices G