for G being _finite _Graph holds (MCS:CSeq G) ``1 is eventually-constant