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