let am, bp, cm, dp, cin be set ; :: thesis: 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; :: thesis: verum