let x, y, z be set ; :: thesis: InnerVertices (GFA3CarryIStr (x,y,z)) = {[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]}
set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set xy = [<*x,y*>,and2b];
set yz = [<*y,z*>,and2b];
set zx = [<*z,x*>,and2b];
set Cxy = 1GateCircStr (<*x,y*>,and2b);
set Cyz = 1GateCircStr (<*y,z*>,and2b);
set Czx = 1GateCircStr (<*z,x*>,and2b);
A1: 1GateCircStr (<*x,y*>,and2b) tolerates 1GateCircStr (<*y,z*>,and2b) by CIRCCOMB:55;
(1GateCircStr (<*x,y*>,and2b)) +* (1GateCircStr (<*y,z*>,and2b)) tolerates 1GateCircStr (<*z,x*>,and2b) by CIRCCOMB:55;
then InnerVertices (GFA3CarryIStr (x,y,z)) = (InnerVertices ((1GateCircStr (<*x,y*>,and2b)) +* (1GateCircStr (<*y,z*>,and2b)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2b))) by CIRCCOMB:15
.= ((InnerVertices (1GateCircStr (<*x,y*>,and2b))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2b)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2b))) by A1, CIRCCOMB:15
.= ({[<*x,y*>,and2b]} \/ (InnerVertices (1GateCircStr (<*y,z*>,and2b)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2b))) by CIRCCOMB:49
.= ({[<*x,y*>,and2b]} \/ {[<*y,z*>,and2b]}) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2b))) by CIRCCOMB:49
.= ({[<*x,y*>,and2b]} \/ {[<*y,z*>,and2b]}) \/ {[<*z,x*>,and2b]} by CIRCCOMB:49
.= {[<*x,y*>,and2b],[<*y,z*>,and2b]} \/ {[<*z,x*>,and2b]} by ENUMSET1:41
.= {[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]} by ENUMSET1:43 ;
hence InnerVertices (GFA3CarryIStr (x,y,z)) = {[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]} ; :: thesis: verum