let x be object ; :: according to GLPACY00:def 2 :: thesis: ( x in dom <*P*> implies ex G being _Graph st
( <*P*> . x = G & G is Path-like ) )
assume A1: x in dom <*P*> ; :: thesis: ex G being _Graph st
( <*P*> . x = G & G is Path-like )
then reconsider n = x as Nat ;
( 1 <= n & n <= len <*P*> ) by A1, FINSEQ_3:25;
then ( 1 <= n & n <= 1 ) by FINSEQ_1:40;
then n = 1 by XXREAL_0:1;
hence ex G being _Graph st
( <*P*> . x = G & G is Path-like ) ; :: thesis: verum