theorem :: MSAFREE2:4

for G being non empty ManySortedSign holds InputVertices G misses SortsWithConstants G