theorem :: FTACELL1:2

for ap, bp, cp, dp, cin being set holds InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) is Relation