let am, bm, cm, dm, cin be set ; :: thesis: InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) is Relation
set S1 = BitGFA3Str (am,bm,cm);
set A1 = GFA3AdderOutput (am,bm,cm);
set S2 = BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm);
( InnerVertices (BitGFA3Str (am,bm,cm)) is Relation & InnerVertices (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) is Relation ) by GFACIRC1:128;
hence InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) is Relation by FACIRC_1:3; :: thesis: verum