let x, y, z be set ; :: thesis: InnerVertices (BitGFA1Str x,y,z) is Relation
set S1 = GFA1AdderStr x,y,z;
set S2 = GFA1CarryStr x,y,z;
( InnerVertices (GFA1AdderStr x,y,z) is Relation & InnerVertices (GFA1CarryStr x,y,z) is Relation ) by Th51, FACIRC_1:58;
hence InnerVertices (BitGFA1Str x,y,z) is Relation by FACIRC_1:3; :: thesis: verum