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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum