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