let x, y, z be set ; :: thesis: InnerVertices (BitGFA2Str (x,y,z)) is Relation
set S1 = GFA2AdderStr (x,y,z);
set S2 = GFA2CarryStr (x,y,z);
( InnerVertices (GFA2AdderStr (x,y,z)) is Relation & InnerVertices (GFA2CarryStr (x,y,z)) is Relation ) by Th75, FACIRC_1:58;
hence InnerVertices (BitGFA2Str (x,y,z)) is Relation by FACIRC_1:3; :: thesis: verum