let x, y, c be non pair set ; :: thesis: InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c}
set S = BitSubtracterWithBorrowStr (x,y,c);
set S1 = 2GatesCircStr (x,y,c,'xor');
set S2 = BorrowStr (x,y,c);
A1: ( InputVertices (2GatesCircStr (x,y,c,'xor')) = {x,y,c} & InputVertices (BorrowStr (x,y,c)) = {x,y,c} ) by Th9, FACIRC_1:57;
( InnerVertices (2GatesCircStr (x,y,c,'xor')) is Relation & InnerVertices (BorrowStr (x,y,c)) is Relation ) by Th1, FACIRC_1:58;
hence InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c} \/ {x,y,c} by A1, FACIRC_1:7
.= {x,y,c} ;
:: thesis: verum