let x, y, c be set ; :: thesis: InnerVertices (BitAdderWithOverflowStr x,y,c) is Relation
( InnerVertices (2GatesCircStr x,y,c,'xor' ) is Relation & InnerVertices (MajorityStr x,y,c) is Relation ) by Th58, Th67;
hence InnerVertices (BitAdderWithOverflowStr x,y,c) is Relation by Th2, CIRCCOMB:55; :: thesis: verum