theorem Th85: :: FACIRC_1:85

for x, y, c being non pair object holds InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c}