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