theorem Th33: :: FTACELL1:33

for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & not cin in InnerVertices (BitGFA3Str (am,bm,cm)) holds
InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) = {am,bm,cm,dm,cin}