let G be non empty ManySortedSign ; :: thesis: InputVertices G misses SortsWithConstants G
( InputVertices G misses InnerVertices G & SortsWithConstants G c= InnerVertices G ) by Th5, XBOOLE_1:79;
hence InputVertices G misses SortsWithConstants G by XBOOLE_1:63; :: thesis: verum