let G be _finite _Graph; :: thesis: LexBFS:CSeq G is iterative
set CS = LexBFS:CSeq G;
let k, n be Nat; :: according to LEXBFS:def 6 :: thesis: ( (LexBFS:CSeq G) . k = (LexBFS:CSeq G) . n implies (LexBFS:CSeq G) . (k + 1) = (LexBFS:CSeq G) . (n + 1) )
assume A1: (LexBFS:CSeq G) . k = (LexBFS:CSeq G) . n ; :: thesis: (LexBFS:CSeq G) . (k + 1) = (LexBFS:CSeq G) . (n + 1)
(LexBFS:CSeq G) . (k + 1) = LexBFS:Step ((LexBFS:CSeq G) . k) by Def16;
hence (LexBFS:CSeq G) . (k + 1) = (LexBFS:CSeq G) . (n + 1) by A1, Def16; :: thesis: verum