let X be set ; :: thesis: for G being finite Graph
for v being Vertex of G
for p being Element of X -PathSet v
for Y being finite set st Y = the carrier' of G & Degree (v,X) <> 0 holds
len p <= card Y
let G be finite Graph; :: thesis: for v being Vertex of G
for p being Element of X -PathSet v
for Y being finite set st Y = the carrier' of G & Degree (v,X) <> 0 holds
len p <= card Y
let v be Vertex of G; :: thesis: for p being Element of X -PathSet v
for Y being finite set st Y = the carrier' of G & Degree (v,X) <> 0 holds
len p <= card Y
let p be Element of X -PathSet v; :: thesis: for Y being finite set st Y = the carrier' of G & Degree (v,X) <> 0 holds
len p <= card Y
let Y be finite set ; :: thesis: ( Y = the carrier' of G & Degree (v,X) <> 0 implies len p <= card Y )
assume that
A1: Y = the carrier' of G and
A2: Degree (v,X) <> 0 ; :: thesis: len p <= card Y
A3: p in X -PathSet v ;
X -PathSet v = { c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } by A2, Def11;
then ex c being Element of X * st
( p = c & c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) by A3;
then A4: card (rng p) = len p by FINSEQ_4:62;
rng p c= Y by A1, FINSEQ_1:def 4;
hence len p <= card Y by A4, NAT_1:43; :: thesis: verum