theorem Th15: :: FACIRC_1:15
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following (s,2) = Following (Following s)