let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G

for n, m being Nat st (S .Lifespan()) -' n < m & m <= S .Lifespan() holds

ex v being Vertex of G st

( v in dom (S . n) & (S . n) . v = m )

let S be VNumberingSeq of G; :: thesis: for n, m being Nat st (S .Lifespan()) -' n < m & m <= S .Lifespan() holds

ex v being Vertex of G st

( v in dom (S . n) & (S . n) . v = m )

let n, m be Nat; :: thesis: ( (S .Lifespan()) -' n < m & m <= S .Lifespan() implies ex v being Vertex of G st

( v in dom (S . n) & (S . n) . v = m ) )

assume that

A1: (S .Lifespan()) -' n < m and

A2: m <= S .Lifespan() ; :: thesis: ex v being Vertex of G st

( v in dom (S . n) & (S . n) . v = m )

set CSN = S . n;

set VLN = S . n;

m in (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' n)) by A1, A2, Th3;

then m in rng (S . n) by Th14;

then consider v being object such that

A3: v in dom (S . n) and

A4: m = (S . n) . v by FUNCT_1:def 3;

reconsider v = v as set by TARSKI:1;

take v ; :: thesis: ( v is Vertex of G & v in dom (S . n) & (S . n) . v = m )

thus v is Vertex of G by A3; :: thesis: ( v in dom (S . n) & (S . n) . v = m )

thus v in dom (S . n) by A3; :: thesis: (S . n) . v = m

thus (S . n) . v = m by A4; :: thesis: verum

for n, m being Nat st (S .Lifespan()) -' n < m & m <= S .Lifespan() holds

ex v being Vertex of G st

( v in dom (S . n) & (S . n) . v = m )

let S be VNumberingSeq of G; :: thesis: for n, m being Nat st (S .Lifespan()) -' n < m & m <= S .Lifespan() holds

ex v being Vertex of G st

( v in dom (S . n) & (S . n) . v = m )

let n, m be Nat; :: thesis: ( (S .Lifespan()) -' n < m & m <= S .Lifespan() implies ex v being Vertex of G st

( v in dom (S . n) & (S . n) . v = m ) )

assume that

A1: (S .Lifespan()) -' n < m and

A2: m <= S .Lifespan() ; :: thesis: ex v being Vertex of G st

( v in dom (S . n) & (S . n) . v = m )

set CSN = S . n;

set VLN = S . n;

m in (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' n)) by A1, A2, Th3;

then m in rng (S . n) by Th14;

then consider v being object such that

A3: v in dom (S . n) and

A4: m = (S . n) . v by FUNCT_1:def 3;

reconsider v = v as set by TARSKI:1;

take v ; :: thesis: ( v is Vertex of G & v in dom (S . n) & (S . n) . v = m )

thus v is Vertex of G by A3; :: thesis: ( v in dom (S . n) & (S . n) . v = m )

thus v in dom (S . n) by A3; :: thesis: (S . n) . v = m

thus (S . n) . v = m by A4; :: thesis: verum