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 ( 1 <= n & n < len IT ) ; :: thesis: ex e being set st e Joins IT . n,IT . (n + 1),G
hence ex e being set st e Joins IT . n,IT . (n + 1),G by FINSEQ_1:57; :: thesis: verum