let ap, bm, cp, dm, cin be set ; :: thesis: InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) is Relation
set S = BitFTA1Str ap,bm,cp,dm,cin;
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:77, GFACIRC1:114;
hence InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) is Relation by FACIRC_1:3; :: thesis: verum