let S be non empty unsplit ManySortedSign ; :: thesis: InnerVertices S = the carrier' of S
the ResultSort of S = id the carrier' of S by CIRCCOMB:def 7;
hence InnerVertices S = the carrier' of S ; :: thesis: verum