per cases ( n >= S .Lifespan() or n < S .Lifespan() ) ;

suppose n >= S .Lifespan() ; :: thesis: ( ( n >= S .Lifespan() implies ex b₁ being set st b₁ = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b₁ being set st
( not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan()) -' n)) ) ) )

hence ( ( n >= S .Lifespan() implies ex b₁ being set st b₁ = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b₁ being set st
( not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan()) -' n)) ) ) ) ; :: thesis: verum

end;

suppose n < S .Lifespan() ; :: thesis: ( ( n >= S .Lifespan() implies ex b₁ being set st b₁ = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b₁ being set st
( not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan()) -' n)) ) ) )

then ex w being Vertex of G st
( not w in dom (S . n) & S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) ) by Def8;
hence ( ( n >= S .Lifespan() implies ex b₁ being set st b₁ = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b₁ being set st
( not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan()) -' n)) ) ) ) ; :: thesis: verum

end;

end;