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