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