theorem :: FACIRC_1:87

for x, y, c being object
for S being non empty ManySortedSign st S = BitAdderWithOverflowStr (x,y,c) holds
( x in the carrier of S & y in the carrier of S & c in the carrier of S )