let ap, bp, cp, dp, cin be set ; InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) is Relation
set S1 = BitGFA0Str (ap,bp,cp);
set A1 = GFA0AdderOutput (ap,bp,cp);
set S2 = BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp);
( InnerVertices (BitGFA0Str (ap,bp,cp)) is Relation & InnerVertices (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) is Relation )
by GFACIRC1:32;
hence
InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) is Relation
by FACIRC_1:3; verum