let G be _finite _Graph; :: thesis: (LexBFS:CSeq G) ``1 is eventually-constant
set CS = LexBFS:CSeq G;
set S = (LexBFS:CSeq G) ``1 ;

now :: thesis: ex n being Nat st
for m being Nat st n <= m holds
((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m

consider n being Nat such that
A1: for m being Nat st n <= m holds
(LexBFS:CSeq G) . n = (LexBFS:CSeq G) . m by Def6;
take n = n; :: thesis: for m being Nat st n <= m holds
((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m
let m be Nat; :: thesis: ( n <= m implies ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m )
assume A2: n <= m ; :: thesis: ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m
thus ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) . n) `1 by Def15
.= ((LexBFS:CSeq G) . m) `1 by A1, A2
.= ((LexBFS:CSeq G) ``1) . m by Def15 ; :: thesis: verum

end;

hence (LexBFS:CSeq G) ``1 is eventually-constant ; :: thesis: verum