take {} ; :: thesis: ( ( for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n in the carrier' of G ) & ex p being FinSequence st
( len p = (len {} ) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds
ex x', y' being Vertex of G st
( x' = p . n & y' = p . (n + 1) & {} . n joins x',y' ) ) ) )
thus for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n in the carrier' of G by XXREAL_0:2; :: thesis: ex p being FinSequence st
( len p = (len {} ) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds
ex x', y' being Vertex of G st
( x' = p . n & y' = p . (n + 1) & {} . n joins x',y' ) ) )
consider x being Vertex of G;
A1: x in the carrier of G ;
take <*x*> ; :: thesis: ( len <*x*> = (len {} ) + 1 & ( for n being Element of NAT st 1 <= n & n <= len <*x*> holds
<*x*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds
ex x', y' being Vertex of G st
( x' = <*x*> . n & y' = <*x*> . (n + 1) & {} . n joins x',y' ) ) )
thus len <*x*> = (len {} ) + 1 by FINSEQ_1:56; :: thesis: ( ( for n being Element of NAT st 1 <= n & n <= len <*x*> holds
<*x*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds
ex x', y' being Vertex of G st
( x' = <*x*> . n & y' = <*x*> . (n + 1) & {} . n joins x',y' ) ) )
thus for n being Element of NAT st 1 <= n & n <= len <*x*> holds
<*x*> . n in the carrier of G :: thesis: for n being Element of NAT st 1 <= n & n <= len {} holds
ex x', y' being Vertex of G st
( x' = <*x*> . n & y' = <*x*> . (n + 1) & {} . n joins x',y' )

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len <*x*> implies <*x*> . n in the carrier of G )
assume ( 1 <= n & n <= len <*x*> ) ; :: thesis: <*x*> . n in the carrier of G
then ( 1 <= n & n <= 1 ) by FINSEQ_1:56;
then n = 1 by XXREAL_0:1;
hence <*x*> . n in the carrier of G by A1, FINSEQ_1:57; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len {} implies ex x', y' being Vertex of G st
( x' = <*x*> . n & y' = <*x*> . (n + 1) & {} . n joins x',y' ) )
thus ( 1 <= n & n <= len {} implies ex x', y' being Vertex of G st
( x' = <*x*> . n & y' = <*x*> . (n + 1) & {} . n joins x',y' ) ) by XXREAL_0:2; :: thesis: verum