theorem Th4: :: CIRCCMB2:4

for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n1, n2 being natural Number st Following (s,n1) is stable & n1 <= n2 holds
Following (s,n2) = Following (s,n1)