let am, bp, cm, dp, cin be set ; InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) is Relation
set S1 = BitGFA2Str (am,bp,cm);
set A1 = GFA2AdderOutput (am,bp,cm);
set S2 = BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp);
( InnerVertices (BitGFA2Str (am,bp,cm)) is Relation & InnerVertices (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) is Relation )
by GFACIRC1:64, GFACIRC1:96;
hence
InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) is Relation
by FACIRC_1:3; verum