let x, y, z be set ; :: thesis: InnerVertices (GFA3CarryStr (x,y,z)) is Relation
set f1 = nor2 ;
set f2 = nor2 ;
set f3 = nor2 ;
set f4 = nor3 ;
set xy = [<*x,y*>,nor2];
set yz = [<*y,z*>,nor2];
set zx = [<*z,x*>,nor2];
set Cxy = 1GateCircStr (<*x,y*>,nor2);
set Cyz = 1GateCircStr (<*y,z*>,nor2);
set Czx = 1GateCircStr (<*z,x*>,nor2);
set Cxyz = 1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3);
( InnerVertices (1GateCircStr (<*x,y*>,nor2)) is Relation & InnerVertices (1GateCircStr (<*y,z*>,nor2)) is Relation ) by FACIRC_1:38;
then ( InnerVertices (1GateCircStr (<*z,x*>,nor2)) is Relation & InnerVertices ((1GateCircStr (<*x,y*>,nor2)) +* (1GateCircStr (<*y,z*>,nor2))) is Relation ) by FACIRC_1:3, FACIRC_1:38;
then ( InnerVertices (1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,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