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