set v = the Element of the_Vertices_of G;
set IT = <* the Element of the_Vertices_of G*>;
reconsider IT = <* the Element of the_Vertices_of G*> as FinSequence of the_Vertices_of G ;
take
IT
; for n being Element of NAT st 1 <= n & n < len IT holds
ex e being set st e Joins IT . n,IT . (n + 1),G
let n be Element of NAT ; ( 1 <= n & n < len IT implies ex e being set st e Joins IT . n,IT . (n + 1),G )
assume that
A1:
1 <= n
and
A2:
n < len IT
; ex e being set st e Joins IT . n,IT . (n + 1),G
thus
ex e being set st e Joins IT . n,IT . (n + 1),G
by A1, A2, FINSEQ_1:40; verum