let x, y, z be set ; :: thesis: InnerVertices (GFA3CarryStr (x,y,z)) is Relation
set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set f4 = nor3 ;
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);
set Cxyz = 1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3);
( InnerVertices (1GateCircStr (<*x,y*>,and2b)) is Relation & InnerVertices (1GateCircStr (<*y,z*>,and2b)) is Relation ) by FACIRC_1:38;
then ( InnerVertices (1GateCircStr (<*z,x*>,and2b)) is Relation & InnerVertices ((1GateCircStr (<*x,y*>,and2b)) +* (1GateCircStr (<*y,z*>,and2b))) is Relation ) by FACIRC_1:3, FACIRC_1:38;
then ( InnerVertices (1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3)) is Relation & InnerVertices (GFA3CarryIStr (x,y,z)) is Relation ) by FACIRC_1:3, FACIRC_1:38;
hence InnerVertices (GFA3CarryStr (x,y,z)) is Relation by FACIRC_1:3; :: thesis: verum