:: deftheorem defines BitSubtracterWithBorrowCirc FSCIRC_1:def 9 :
for x, y, c being set holds BitSubtracterWithBorrowCirc (x,y,c) = (BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c));