let G be non empty ManySortedSign ; :: thesis: InputVertices G misses SortsWithConstants G
InputVertices G misses InnerVertices G by XBOOLE_1:79;
hence InputVertices G misses SortsWithConstants G by Th3, XBOOLE_1:63; :: thesis: verum