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

the ResultSort of S = id the carrier' of S by CIRCCOMB:def 7;

hence InnerVertices S = the carrier' of S ; :: thesis: verum