let x, y, z be set ; InnerVertices (BitGFA0Str (x,y,z)) is Relation
set S1 = GFA0AdderStr (x,y,z);
set S2 = GFA0CarryStr (x,y,z);
( InnerVertices (GFA0AdderStr (x,y,z)) is Relation & InnerVertices (GFA0CarryStr (x,y,z)) is Relation )
by Th12, FACIRC_1:58;
hence
InnerVertices (BitGFA0Str (x,y,z)) is Relation
by FACIRC_1:3; verum