let G be _Graph; :: thesis: for W being Walk of G st W is V5() 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 V5() implies for v being Vertex of G st v in W .vertices() holds
not v is isolated )
assume W is V5() ; :: 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;
end;
end;
hence not v is isolated by GLIB_000:def 49; :: thesis: verum