let x, y, c be set ; 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]}
; verum