let G be _Graph; :: thesis: for W being Walk of G st not W is trivial holds

for v being Vertex of G st v in W .vertices() holds

not v is isolated

let W be Walk of G; :: thesis: ( not W is trivial implies for v being Vertex of G st v in W .vertices() holds

not v is isolated )

assume not W is trivial ; :: thesis: for v being Vertex of G st v in W .vertices() holds

not v is isolated

then A1: len W <> 1 by Lm55;

let v be Vertex of G; :: thesis: ( v in W .vertices() implies not v is isolated )

assume v in W .vertices() ; :: thesis: not v is isolated

then consider n being odd Element of NAT such that

A2: n <= len W and

A3: W . n = v by Lm45;

for v being Vertex of G st v in W .vertices() holds

not v is isolated

let W be Walk of G; :: thesis: ( not W is trivial implies for v being Vertex of G st v in W .vertices() holds

not v is isolated )

assume not W is trivial ; :: thesis: for v being Vertex of G st v in W .vertices() holds

not v is isolated

then A1: len W <> 1 by Lm55;

let v be Vertex of G; :: thesis: ( v in W .vertices() implies not v is isolated )

assume v in W .vertices() ; :: thesis: not v is isolated

then consider n being odd Element of NAT such that

A2: n <= len W and

A3: W . n = v by Lm45;

now :: thesis: ex e being set st e in v .edgesInOut() end;

hence
not v is isolated
by GLIB_000:def 49; :: thesis: verumper cases
( n = len W or n <> len W )
;

end;

suppose A4:
n = len W
; :: thesis: ex e being set st e in v .edgesInOut()

1 <= len W
by ABIAN:12;

then 1 < len W by A1, XXREAL_0:1;

then 1 + 1 <= len W by NAT_1:13;

then reconsider lenW2 = (len W) - (2 * 1) as odd Element of NAT by INT_1:5;

lenW2 < (len W) - 0 by XREAL_1:15;

then W . (lenW2 + 1) Joins W . lenW2,W . (lenW2 + 2),G by Def3;

then W . (lenW2 + 1) Joins v,W . lenW2,G by A3, A4, GLIB_000:14;

hence ex e being set st e in v .edgesInOut() by GLIB_000:62; :: thesis: verum

end;then 1 < len W by A1, XXREAL_0:1;

then 1 + 1 <= len W by NAT_1:13;

then reconsider lenW2 = (len W) - (2 * 1) as odd Element of NAT by INT_1:5;

lenW2 < (len W) - 0 by XREAL_1:15;

then W . (lenW2 + 1) Joins W . lenW2,W . (lenW2 + 2),G by Def3;

then W . (lenW2 + 1) Joins v,W . lenW2,G by A3, A4, GLIB_000:14;

hence ex e being set st e in v .edgesInOut() by GLIB_000:62; :: thesis: verum

suppose
n <> len W
; :: thesis: ex e being set st e in v .edgesInOut()

then
n < len W
by A2, XXREAL_0:1;

then W . (n + 1) Joins v,W . (n + 2),G by A3, Def3;

hence ex e being set st e in v .edgesInOut() by GLIB_000:62; :: thesis: verum

end;then W . (n + 1) Joins v,W . (n + 2),G by A3, Def3;

hence ex e being set st e in v .edgesInOut() by GLIB_000:62; :: thesis: verum