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