theorem :: FTACELL1:32
for am, bm, cm, dm, cin being set holds InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) is Relation