theorem :: FTACELL1:12

for ap, bm, cp, dm, cin being set holds InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) is Relation