theorem Th18: :: FTACELL2:18

for n being Nat
for ap, bm, cp, dm being nonpair-yielding FinSequence holds InputVertices (n -BitFTA1Layer1Str (ap,bm,cp)) misses InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))