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