let G be _Graph; :: thesis: for S being set
for v being Vertex of G st not v in S & S meets G .reachableFrom v holds
G .AdjacentSet S <> {}
let S be set ; :: thesis: for v being Vertex of G st not v in S & S meets G .reachableFrom v holds
G .AdjacentSet S <> {}
let v be Vertex of G; :: thesis: ( not v in S & S meets G .reachableFrom v implies G .AdjacentSet S <> {} )
assume A1: ( not v in S & S meets G .reachableFrom v ) ; :: thesis: G .AdjacentSet S <> {}
then consider w being object such that
A2: ( w in S & w in G .reachableFrom v ) by XBOOLE_0:3;
consider W being Walk of G such that
A3: W is_Walk_from v,w by A2, GLIB_002:def 5;
ex n being odd Nat st
( n < len W & not W . n in S & W . (n + 2) in S )
proof
assume A4: for n being odd Nat holds
( n >= len W or W . n in S or not W . (n + 2) in S ) ; :: thesis: contradiction
defpred S1[ Nat] means ( (2 * $1) + 1 <= len W implies not W . ((2 * $1) + 1) in S );
A5: S1[ 0 ]
proof
assume (2 * 0) + 1 <= len W ; :: thesis: not W . ((2 * 0) + 1) in S
W . ((2 * 0) + 1) = W .first() by GLIB_001:def 6
.= v by A3, GLIB_001:def 23 ;
hence not W . ((2 * 0) + 1) in S by A1; :: thesis: verum
end;
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: ( S1[k] & (2 * (k + 1)) + 1 <= len W ) ; :: thesis: not W . ((2 * (k + 1)) + 1) in S
k + 0 < k + 1 by XREAL_1:8;
then 2 * k < 2 * (k + 1) by XREAL_1:68;
then (2 * k) + 1 < (2 * (k + 1)) + 1 by XREAL_1:8;
then (2 * k) + 1 < len W by A7, XXREAL_0:2;
then not W . (((2 * k) + 1) + 2) in S by A4, A7;
hence not W . ((2 * (k + 1)) + 1) in S ; :: thesis: verum
end;
A8: for k being Nat holds S1[k] from NAT_1:sch 2(A5, A6);
 reconsider m = (len W) - 1 as Nat by CHORD:2;
set k = m div 2;
m = 2 * (m div 2) by ABIAN:def 1, NAT_D:3;
then (2 * (m div 2)) + 1 = len W ;
then not W . (len W) in S by A8;
then not W .last() in S by GLIB_001:def 7;
hence contradiction by A2, A3, GLIB_001:def 23; :: thesis: verum
end;
then consider n being odd Nat such that
A9: ( n < len W & not W . n in S & W . (n + 2) in S ) ;
n is odd Element of NAT by ORDINAL1:def 12;
then A10: W . (n + 1) Joins W . n,W . (n + 2),G by A9, GLIB_001:def 3;
then reconsider u1 = W . n, u2 = W . (n + 2) as Vertex of G by GLIB_000:13;
u1,u2 are_adjacent by A10, CHORD:def 3;
hence G .AdjacentSet S <> {} by A9, CHORD:50; :: thesis: verum