theorem :: FACIRC_1:88

for x, y, c being object holds InnerVertices (BitAdderWithOverflowStr (x,y,c)) is Relation