let ap, bm, cp, dm, cin be set ; :: thesis: InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) is Relation
set S1 = BitGFA1Str (ap,bm,cp);
set A1 = GFA1AdderOutput (ap,bm,cp);
set S2 = BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm);
( InnerVertices (BitGFA1Str (ap,bm,cp)) is Relation & InnerVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) is Relation ) by GFACIRC1:64, GFACIRC1:96;
hence InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) is Relation by FACIRC_1:3; :: thesis: verum