let x, y, c be 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 )
set S1 = 2GatesCircStr (x,y,c,'xor');
let S be non empty ManySortedSign ; ( S = BitSubtracterWithBorrowStr (x,y,c) implies ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) )
A1:
( x in the carrier of (2GatesCircStr (x,y,c,'xor')) & y in the carrier of (2GatesCircStr (x,y,c,'xor')) )
by FACIRC_1:60;
A2:
c in the carrier of (2GatesCircStr (x,y,c,'xor'))
by FACIRC_1:60;
assume
S = BitSubtracterWithBorrowStr (x,y,c)
; ( x in the carrier of S & y in the carrier of S & c in the carrier of S )
hence
( x in the carrier of S & y in the carrier of S & c in the carrier of S )
by A1, A2, FACIRC_1:20; verum