theorem :: FSCIRC_1:23

for x, y, c being non pair set holds InputVertices (BitSubtracterWithBorrowStr (x,y,c)) is without_pairs