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