let x, y, c be set ; :: thesis: InnerVertices (BitSubtracterWithBorrowStr x,y,c) is Relation
( InnerVertices (2GatesCircStr x,y,c,'xor' ) is Relation & InnerVertices (BorrowStr x,y,c) is Relation ) by Th1, FACIRC_1:58;
hence InnerVertices (BitSubtracterWithBorrowStr x,y,c) is Relation by FACIRC_1:3; :: thesis: verum