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

end;

suppose
n >= S .Lifespan()
; :: thesis: ( ( n >= S .Lifespan() implies ex b_{1} being set st b_{1} = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b_{1} being set st

( not b_{1} in dom (S . n) & S . (n + 1) = (S . n) +* (b_{1} .--> ((S .Lifespan()) -' n)) ) ) )

( not b

hence
( ( n >= S .Lifespan() implies ex b_{1} being set st b_{1} = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b_{1} being set st

( not b_{1} in dom (S . n) & S . (n + 1) = (S . n) +* (b_{1} .--> ((S .Lifespan()) -' n)) ) ) )
; :: thesis: verum

end;( not b

suppose
n < S .Lifespan()
; :: thesis: ( ( n >= S .Lifespan() implies ex b_{1} being set st b_{1} = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b_{1} being set st

( not b_{1} in dom (S . n) & S . (n + 1) = (S . n) +* (b_{1} .--> ((S .Lifespan()) -' n)) ) ) )

( not b

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_{1} being set st b_{1} = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b_{1} being set st

( not b_{1} in dom (S . n) & S . (n + 1) = (S . n) +* (b_{1} .--> ((S .Lifespan()) -' n)) ) ) )
; :: thesis: verum

end;( not w in dom (S . n) & S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) ) by Def8;

hence ( ( n >= S .Lifespan() implies ex b

( not b