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