let A be non-empty Circuit of S; :: thesis: ( A is with_stabilization-limit implies A is stabilizing )
given n being Element of NAT such that A1: for s being State of A holds Following (s,n) is stable ; :: according to CIRCCMB3:def 3 :: thesis: A is stabilizing
let s be State of A; :: according to CIRCCMB3:def 2 :: thesis: s is stabilizing
take n ; :: according to CIRCCMB3:def 1 :: thesis: Following (s,n) is stable
thus Following (s,n) is stable by A1; :: thesis: verum