let G be _finite _Graph; :: thesis: (MCS:CSeq G) .Lifespan() = G .order()
set CS = MCS:CSeq G;
A1: for n being Nat st (MCS:CSeq G) . n = (MCS:CSeq G) . (n + 1) holds
G .order() <= n

proof

let n be Nat; :: thesis: ( (MCS:CSeq G) . n = (MCS:CSeq G) . (n + 1) implies G .order() <= n )
assume A2: (MCS:CSeq G) . n = (MCS:CSeq G) . (n + 1) ; :: thesis: G .order() <= n
set w = MCS:PickUnnumbered ((MCS:CSeq G) . n);
set VN1 = ((MCS:CSeq G) . (n + 1)) `1 ;
set VLN = ((MCS:CSeq G) . n) `1 ;
set j = card (dom (((MCS:CSeq G) . n) `1));
set wf = (MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((MCS:CSeq G) . n) `1))));
assume A3: n < G .order() ; :: thesis: contradiction
then dom (((MCS:CSeq G) . n) `1) <> the_Vertices_of G by Th69;
then A4: not MCS:PickUnnumbered ((MCS:CSeq G) . n) in dom (((MCS:CSeq G) . n) `1) by Th59;
card (dom (((MCS:CSeq G) . n) `1)) < G .order() by A3, Th65;
then A5: ((MCS:CSeq G) . (n + 1)) `1 = (((MCS:CSeq G) . n) `1) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((MCS:CSeq G) . n) `1))))) by Th64;
dom ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((MCS:CSeq G) . n) `1))))) = {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} ;
then A6: dom (((MCS:CSeq G) . (n + 1)) `1) = (dom (((MCS:CSeq G) . n) `1)) \/ {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} by A5, FUNCT_4:def 1;
MCS:PickUnnumbered ((MCS:CSeq G) . n) in {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} by TARSKI:def 1;
hence contradiction by A2, A4, A6, XBOOLE_0:def 3; :: thesis: verum

end;

G .order() <= (G .order()) + 1 by NAT_1:13;
then (MCS:CSeq G) . (G .order()) = (MCS:CSeq G) . ((G .order()) + 1) by Th66;
hence (MCS:CSeq G) .Lifespan() = G .order() by A1, GLIB_000:def 56; :: thesis: verum