let G be _Graph; :: thesis: for W being Walk of G st 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: ( W is trivial implies for v being Vertex of G st v in W .vertices() holds
not v is isolated )
assume 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()

per cases ( n = len W or n <> len W ) ;

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;

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;

end;

end;

hence not v is isolated by GLIB_000:def 49; :: thesis: verum