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: ( not InputVertices (2GatesCircStr x,y,c,'xor' ) is with_pair & InnerVertices (2GatesCircStr x,y,c,'xor' ) is Relation ) by FACIRC_1:58, FACIRC_1:59;
A2: ( not InputVertices (BorrowStr x,y,c) is with_pair & InnerVertices (BorrowStr x,y,c) is Relation ) by Th1, Th2;
( InputVertices (2GatesCircStr x,y,c,'xor' ) = {x,y,c} & InputVertices (BorrowStr x,y,c) = {x,y,c} ) by Th9, FACIRC_1:57;
hence InputVertices (BitSubtracterWithBorrowStr x,y,c) = {x,y,c} \/ {x,y,c} by A1, A2, FACIRC_1:7
.= {x,y,c} ;
:: thesis: verum