let G be finite _Graph; :: thesis: (LexBFS:CSeq G) .Lifespan() = G .order()
set CS = LexBFS:CSeq G;
G .order() <= (G .order() ) + 1 by NAT_1:13;
then A1: (LexBFS:CSeq G) . (G .order() ) = (LexBFS:CSeq G) . ((G .order() ) + 1) by Th47;
for n being Nat st (LexBFS:CSeq G) . n = (LexBFS:CSeq G) . (n + 1) holds
G .order() <= n

proof

let n be Nat; :: thesis: ( (LexBFS:CSeq G) . n = (LexBFS:CSeq G) . (n + 1) implies G .order() <= n )
assume A2: (LexBFS:CSeq G) . n = (LexBFS:CSeq G) . (n + 1) ; :: thesis: G .order() <= n
assume A3: n < G .order() ; :: thesis: contradiction
set VLN = ((LexBFS:CSeq G) . n) `1 ;
set VN1 = ((LexBFS:CSeq G) . (n + 1)) `1 ;
set w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n);
set j = card (dom (((LexBFS:CSeq G) . n) `1 ));
dom (((LexBFS:CSeq G) . n) `1 ) <> the_Vertices_of G by A3, Th50;
then A5: not LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) in dom (((LexBFS:CSeq G) . n) `1 ) by Th41;
card (dom (((LexBFS:CSeq G) . n) `1 )) < G .order() by A3, Th46;
then A6: ((LexBFS:CSeq G) . (n + 1)) `1 = (((LexBFS:CSeq G) . n) `1 ) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order() ) -' (card (dom (((LexBFS:CSeq G) . n) `1 ))))) by Th44;
set wf = (LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order() ) -' (card (dom (((LexBFS:CSeq G) . n) `1 ))));
( dom ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order() ) -' (card (dom (((LexBFS:CSeq G) . n) `1 ))))) = {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} & rng ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order() ) -' (card (dom (((LexBFS:CSeq G) . n) `1 ))))) = {((G .order() ) -' (card (dom (((LexBFS:CSeq G) . n) `1 ))))} ) by FUNCOP_1:14, FUNCOP_1:19;
then A7: dom (((LexBFS:CSeq G) . (n + 1)) `1 ) = (dom (((LexBFS:CSeq G) . n) `1 )) \/ {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} by A6, FUNCT_4:def 1;
LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) in {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} by TARSKI:def 1;
hence contradiction by A2, A5, A7, XBOOLE_0:def 3; :: thesis: verum

end;

hence (LexBFS:CSeq G) .Lifespan() = G .order() by A1, GLIB_000:def 57; :: thesis: verum