let G be Graph; :: thesis: {} is Chain of G
thus for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n in the carrier' of G by XXREAL_0:2; :: according to GRAPH_1:def 12 :: 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 x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & {} . n joins x9,y9 ) ) )
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 x9, y9 being Vertex of G st
( x9 = <*x*> . n & y9 = <*x*> . (n + 1) & {} . n joins x9,y9 ) ) )
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 x9, y9 being Vertex of G st
( x9 = <*x*> . n & y9 = <*x*> . (n + 1) & {} . n joins x9,y9 ) ) )
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 x9, y9 being Vertex of G st
( x9 = <*x*> . n & y9 = <*x*> . (n + 1) & {} . n joins x9,y9 )

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len <*x*> implies <*x*> . n in the carrier of G )
assume that
A2: 1 <= n and
A3: n <= len <*x*> ; :: thesis: <*x*> . n in the carrier of G
n <= 1 by A3, FINSEQ_1:56;
then n = 1 by A2, 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 x9, y9 being Vertex of G st
( x9 = <*x*> . n & y9 = <*x*> . (n + 1) & {} . n joins x9,y9 ) )
thus ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st
( x9 = <*x*> . n & y9 = <*x*> . (n + 1) & {} . n joins x9,y9 ) ) by XXREAL_0:2; :: thesis: verum