theorem :: FSCIRC_1:22

for x, y, c being set holds InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) is Relation