let x, y, c be non pair object ; :: thesis: InputVertices (BitAdderWithOverflowStr (x,y,c)) is without_pairs
InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c} by Th85;
hence InputVertices (BitAdderWithOverflowStr (x,y,c)) is without_pairs ; :: thesis: verum