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