let G be finite _Graph; :: thesis: MCS:CSeq G is eventually-constant
take G .order() ; :: according to LEXBFS:def 7 :: thesis: for m being Nat st G .order() <= m holds
(MCS:CSeq G) . (G .order() ) = (MCS:CSeq G) . m
let m be Nat; :: thesis: ( G .order() <= m implies (MCS:CSeq G) . (G .order() ) = (MCS:CSeq G) . m )
assume A1: G .order() <= m ; :: thesis: (MCS:CSeq G) . (G .order() ) = (MCS:CSeq G) . m
thus (MCS:CSeq G) . (G .order() ) = (MCS:CSeq G) . m by A1, Th83; :: thesis: verum