let x, y, c be set ; :: thesis: InnerVertices (BorrowIStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}
A1: (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) tolerates 1GateCircStr (<*x,c*>,and2a) by CIRCCOMB:47;
A2: 1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,c*>,and2) by CIRCCOMB:47;
InnerVertices (BorrowIStr (x,y,c)) = (InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a))) by A1, CIRCCOMB:11
.= ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a))) by A2, CIRCCOMB:11
.= ({[<*x,y*>,and2a]} \/ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a))) by CIRCCOMB:42
.= ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a))) by CIRCCOMB:42
.= ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ {[<*x,c*>,and2a]} by CIRCCOMB:42
.= {[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:1
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by ENUMSET1:3 ;
hence InnerVertices (BorrowIStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} ; :: thesis: verum