let am, bp, cm, dp, cin be set ; :: thesis: InnerVertices (BitFTA2Str am,bp,cm,dp,cin) is Relation
set S = BitFTA2Str am,bp,cm,dp,cin;
set S1 = BitGFA2Str am,bp,cm;
set A1 = GFA2AdderOutput am,bp,cm;
set S2 = BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp;
( InnerVertices (BitGFA2Str am,bp,cm) is Relation & InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp) is Relation ) by GFACIRC1:77, GFACIRC1:114;
hence InnerVertices (BitFTA2Str am,bp,cm,dp,cin) is Relation by FACIRC_1:3; :: thesis: verum