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

consider n being Nat such that
A: for m being Nat st n <= m holds
(LexBFS:CSeq G) . n = (LexBFS:CSeq G) . m by Def16;
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 B: 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 d1stBFSLS
.= ((LexBFS:CSeq G) . m) `1 by A, B
.= ((LexBFS:CSeq G) ``1 ) . m by d1stBFSLS ; :: thesis: verum

end;

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