let G be finite _Graph; :: thesis: ((LexBFS:CSeq G) ``1 ) .Lifespan() = (LexBFS:CSeq G) .Lifespan()
set S = LexBFS:CSeq G;
set VN = (LexBFS:CSeq G) ``1 ;
set ls = G .order() ;
AA: (LexBFS:CSeq G) .Lifespan() = G .order() by Th51;
AHa: (LexBFS:CSeq G) ``1 is eventually-constant by VNS0a;
Aa: ( ((LexBFS:CSeq G) . (G .order() )) `1 = ((LexBFS:CSeq G) ``1 ) . (G .order() ) & ((LexBFS:CSeq G) . ((G .order() ) + 1)) `1 = ((LexBFS:CSeq G) ``1 ) . ((G .order() ) + 1) ) by d1stBFSLS;
A: ((LexBFS:CSeq G) ``1 ) . (G .order() ) = ((LexBFS:CSeq G) ``1 ) . ((G .order() ) + 1) by Th47, Aa, NAT_1:11;

B: now

let n be Nat; :: thesis: ( ((LexBFS:CSeq G) ``1 ) . n = ((LexBFS:CSeq G) ``1 ) . (n + 1) implies not G .order() > n )
assume that
A1: ((LexBFS:CSeq G) ``1 ) . n = ((LexBFS:CSeq G) ``1 ) . (n + 1) and
B1: G .order() > n ; :: thesis: contradiction
n + 1 <= G .order() by B1, NAT_1:13;
then C1: ( card (dom (((LexBFS:CSeq G) . n) `1 )) = n & card (dom (((LexBFS:CSeq G) . (n + 1)) `1 )) = n + 1 ) by B1, Th46;
( ((LexBFS:CSeq G) . n) `1 = ((LexBFS:CSeq G) ``1 ) . n & ((LexBFS:CSeq G) . (n + 1)) `1 = ((LexBFS:CSeq G) ``1 ) . (n + 1) ) by d1stBFSLS;
hence contradiction by C1, A1; :: thesis: verum

end;

thus ((LexBFS:CSeq G) ``1 ) .Lifespan() = (LexBFS:CSeq G) .Lifespan() by AA, AHa, A, B, GLIB_000:def 57; :: thesis: verum