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