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