set v = choose (the_Vertices_of G);
set IT = <*(choose (the_Vertices_of G))*>;
reconsider IT = <*(choose (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