:: deftheorem defines InnerVertices MSAFREE2:def 3 :
for G being non empty ManySortedSign holds InnerVertices G = rng the ResultSort of G;