:: deftheorem Def4 defines with_input_V MSAFREE2:def 4 :
for IT being non empty ManySortedSign holds
( IT is with_input_V iff InputVertices IT <> {} );