let G be _finite _Graph; :: thesis: LexBFS:CSeq G is eventually-constant
take G .order() ; :: according to LEXBFS:def 7 :: thesis: for m being Nat st G .order() <= m holds
(LexBFS:CSeq G) . (G .order()) = (LexBFS:CSeq G) . m
let m be Nat; :: thesis: ( G .order() <= m implies (LexBFS:CSeq G) . (G .order()) = (LexBFS:CSeq G) . m )
assume G .order() <= m ; :: thesis: (LexBFS:CSeq G) . (G .order()) = (LexBFS:CSeq G) . m
hence (LexBFS:CSeq G) . (G .order()) = (LexBFS:CSeq G) . m by Th33; :: thesis: verum