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