let x, y, z be set ; InnerVertices (GFA2CarryStr (x,y,z)) is Relation
set f1 = and2a ;
set f2 = and2c ;
set f3 = nor2 ;
set f4 = nor3 ;
set xy = [<*x,y*>,and2a];
set yz = [<*y,z*>,and2c];
set zx = [<*z,x*>,nor2];
set Cxy = 1GateCircStr (<*x,y*>,and2a);
set Cyz = 1GateCircStr (<*y,z*>,and2c);
set Czx = 1GateCircStr (<*z,x*>,nor2);
set Cxyz = 1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3);
( InnerVertices (1GateCircStr (<*x,y*>,and2a)) is Relation & InnerVertices (1GateCircStr (<*y,z*>,and2c)) is Relation )
by FACIRC_1:38;
then
( InnerVertices (1GateCircStr (<*z,x*>,nor2)) is Relation & InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c))) is Relation )
by FACIRC_1:3, FACIRC_1:38;
then
( InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3)) is Relation & InnerVertices (GFA2CarryIStr (x,y,z)) is Relation )
by FACIRC_1:3, FACIRC_1:38;
hence
InnerVertices (GFA2CarryStr (x,y,z)) is Relation
by FACIRC_1:3; verum