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