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:55;
A2: 1GateCircStr <*x,y*>,and2a tolerates 1GateCircStr <*y,c*>,and2 by CIRCCOMB:55;
InnerVertices (BorrowIStr x,y,c) = (InnerVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 ))) \/ (InnerVertices (1GateCircStr <*x,c*>,and2a )) by A1, CIRCCOMB:15
.= ((InnerVertices (1GateCircStr <*x,y*>,and2a )) \/ (InnerVertices (1GateCircStr <*y,c*>,and2 ))) \/ (InnerVertices (1GateCircStr <*x,c*>,and2a )) by A2, CIRCCOMB:15
.= ({[<*x,y*>,and2a ]} \/ (InnerVertices (1GateCircStr <*y,c*>,and2 ))) \/ (InnerVertices (1GateCircStr <*x,c*>,and2a )) by CIRCCOMB:49
.= ({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]}) \/ (InnerVertices (1GateCircStr <*x,c*>,and2a )) by CIRCCOMB:49
.= ({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]}) \/ {[<*x,c*>,and2a ]} by CIRCCOMB:49
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ]} \/ {[<*x,c*>,and2a ]} by ENUMSET1:41
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} by ENUMSET1:43 ;
hence InnerVertices (BorrowIStr x,y,c) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} ; :: thesis: verum