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

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