for G being _finite _Graph holds (MCS:CSeq G) ``1 is vertex-numbering