theorem Th19: :: FSCIRC_1:19

for x, y, c being non pair set holds InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c}