let ap, bp, cp, dp, cin be set ; :: thesis: InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) is Relation
set S = BitFTA0Str ap,bp,cp,dp,cin;
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:40;
hence InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) is Relation by FACIRC_1:3; :: thesis: verum