let x, y, c be set ; InnerVertices (BorrowStr (x,y,c)) is Relation
( InnerVertices (1GateCircStr (<*x,y*>,and2a)) is Relation & InnerVertices (1GateCircStr (<*y,c*>,and2)) is Relation )
by FACIRC_1:38;
then
( InnerVertices (1GateCircStr (<*x,c*>,and2a)) is Relation & InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is Relation )
by FACIRC_1:3, FACIRC_1:38;
then
( InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation & InnerVertices (BorrowIStr (x,y,c)) is Relation )
by FACIRC_1:3, FACIRC_1:38;
hence
InnerVertices (BorrowStr (x,y,c)) is Relation
by FACIRC_1:3; verum