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 G .order() <= m ; :: thesis: (MCS:CSeq G) . (G .order()) = (MCS:CSeq G) . m
hence (MCS:CSeq G) . (G .order()) = (MCS:CSeq G) . m by Th66; :: thesis: verum