:: deftheorem defines InputVertices MSAFREE2:def 2 :
for G being non empty ManySortedSign holds InputVertices G = the carrier of G \ (rng the ResultSort of G);