let x, b be non pair set ; :: thesis: not InputVertices (IncrementStr (x,b)) is with_pair
InputVertices (IncrementStr (x,b)) = {x,b} by FACIRC_1:40;
hence not InputVertices (IncrementStr (x,b)) is with_pair ; :: thesis: verum