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 A1: ( (S .Lifespan() ) -' n < m & 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, Th5;
then m in rng (S . n) by Th21;
then consider v being set such that
A2: v in dom (S . n) and
A3: m = (S . n) . v by FUNCT_1:def 5;
take v ; :: thesis: ( v is Vertex of G & v in dom (S . n) & (S . n) . v = m )
thus v is Vertex of G by A2; :: thesis: ( v in dom (S . n) & (S . n) . v = m )
thus v in dom (S . n) by A2; :: thesis: (S . n) . v = m
thus (S . n) . v = m by A3; :: thesis: verum