let x, y, c be non pair set ; :: thesis: InputVertices (BitSubtracterWithBorrowStr (x,y,c)) is without_pairs
InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c} by Th19;
hence InputVertices (BitSubtracterWithBorrowStr (x,y,c)) is without_pairs ; :: thesis: verum