now :: thesis: W . (len W) is Vertex of Gend;

hence
W . (len W) is Vertex of G
; :: thesis: verumper cases
( len W = 1 or len W <> 1 )
;

end;

suppose A1:
len W <> 1
; :: thesis: W . (len W) is Vertex of G

1 <= len W
by ABIAN:12;

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

then 1 + 1 < (len W) + 1 by XREAL_1:8;

then 2 <= len W by NAT_1:13;

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

A2: n + 2 = len W ;

then n < len W by NAT_1:16;

then W . (n + 1) Joins W . n,W . (len W),G by A2, Def3;

hence W . (len W) is Vertex of G by GLIB_000:13; :: thesis: verum

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

then 1 + 1 < (len W) + 1 by XREAL_1:8;

then 2 <= len W by NAT_1:13;

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

A2: n + 2 = len W ;

then n < len W by NAT_1:16;

then W . (n + 1) Joins W . n,W . (len W),G by A2, Def3;

hence W . (len W) is Vertex of G by GLIB_000:13; :: thesis: verum