let am, bm, cm, dm, cin be set ; :: thesis: InnerVertices (BitFTA3Str am,bm,cm,dm,cin) is Relation
set S = BitFTA3Str am,bm,cm,dm,cin;
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:151;
hence InnerVertices (BitFTA3Str am,bm,cm,dm,cin) is Relation by FACIRC_1:3; :: thesis: verum