theorem :: FSCIRC_1:21

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