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