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 A1: m <= n ; :: thesis: S . m c= S . n
set CSM = S . m;
set VLM = S . m;
set CSN = S . n;
set VLN = S . n;
defpred S₁[ Nat] means S . m c= S . (m + $1);

A2: now

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;
A4: S . (k + 1) = (S . k) +* ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) by A3, Def27;
set wf = (S .PickedAt k) .--> ((S .Lifespan() ) -' k);
A5: ( dom ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) = {(S .PickedAt k)} & rng ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) = {((S .Lifespan() ) -' k)} ) by FUNCOP_1:14, FUNCOP_1:19;
not S .PickedAt k in dom (S . k) by A3, Def27;
then dom ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) misses dom (S . k) by A5, ZFMISC_1:56;
hence S . k c= S . (k + 1) by A4, FUNCT_4:33; :: 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, Th17; :: thesis: verum

end;

end;

end;

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

proof

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

end;

A10: for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A8);
ex j being Nat st n = m + j by A1, NAT_1:10;
hence S . m c= S . n by A10; :: thesis: verum