let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G
for m, n being Nat st m <= n holds
S . m c= S . n
let S be VNumberingSeq of G; :: thesis: for m, n being Nat st m <= n holds
S . m c= S . n
let m, n be Nat; :: thesis: ( m <= n implies S . m c= S . n )
assume m <= n ; :: thesis: S . m c= S . n
then A1: ex j being Nat st n = m + j by NAT_1:10;
set CSM = S . m;
set VLM = S . m;
defpred S₁[ Nat] means S . m c= S . (m + $1);

A2: now :: thesis: for k being Nat holds S . k c= S . (k + 1)

let k be Nat; :: thesis: S . b₁ c= S . (b₁ + 1)
set CSK = S . k;
set VLK = S . k;
set CK1 = S . (k + 1);
set VK1 = S . (k + 1);

per cases ( k < S .Lifespan() or S .Lifespan() <= k ) ;

suppose A3: k < S .Lifespan() ; :: thesis: S . b₁ c= S . (b₁ + 1)

set w = S .PickedAt k;
set wf = (S .PickedAt k) .--> ((S .Lifespan()) -' k);
not S .PickedAt k in dom (S . k) by A3, Def9;
then A5: dom ((S .PickedAt k) .--> ((S .Lifespan()) -' k)) misses dom (S . k) by ZFMISC_1:50;
S . (k + 1) = (S . k) +* ((S .PickedAt k) .--> ((S .Lifespan()) -' k)) by A3, Def9;
hence S . k c= S . (k + 1) by A5, FUNCT_4:32; :: thesis: verum

end;

suppose A6: S .Lifespan() <= k ; :: thesis: S . b₁ c= S . (b₁ + 1)

k <= k + 1 by NAT_1:13;
hence S . k c= S . (k + 1) by A6, Th10; :: thesis: verum

end;

end;

end;

A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
S . (m + k) c= S . ((m + k) + 1) by A2;
hence S₁[k + 1] by A8, XBOOLE_1:1; :: thesis: verum

end;

A9: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A7);
hence S . m c= S . n by A1; :: thesis: verum