now :: thesis: W . (len W) is Vertex of G
per cases ( len W = 1 or len W <> 1 ) ;
suppose len W = 1 ; :: thesis: W . (len W) is Vertex of G
hence W . (len W) is Vertex of G by Def3; :: thesis: verum
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;
end;
end;
hence W . (len W) is Vertex of G ; :: thesis: verum