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_{1}[ Nat] means S . m c= S . (m + $1);

_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A9, A7);

hence S . m c= S . n by A1; :: thesis: verum

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

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

A7:
for k being Nat st Slet k be Nat; :: thesis: S . b_{1} c= S . (b_{1} + 1)

set CSK = S . k;

set VLK = S . k;

set CK1 = S . (k + 1);

set VK1 = S . (k + 1);

end;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 )
;

end;

suppose A3:
k < S .Lifespan()
; :: thesis: S . b_{1} c= S . (b_{1} + 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;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

S

proof

A9:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A8: S_{1}[k]
; :: thesis: S_{1}[k + 1]

S . (m + k) c= S . ((m + k) + 1) by A2;

hence S_{1}[k + 1]
by A8, XBOOLE_1:1; :: thesis: verum

end;assume A8: S

S . (m + k) c= S . ((m + k) + 1) by A2;

hence S

for k being Nat holds S

hence S . m c= S . n by A1; :: thesis: verum