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