set w = the Element of S;
set v = the Element of (the_Vertices_of G) \ S;
not the_Vertices_of G c= S by SUBSET_1:def 6, XBOOLE_0:def 10;
then (the_Vertices_of G) \ S <> {} by XBOOLE_1:37;
then A1: ( the Element of (the_Vertices_of G) \ S in the_Vertices_of G & not the Element of (the_Vertices_of G) \ S in S ) by XBOOLE_0:def 5;
then reconsider v = the Element of (the_Vertices_of G) \ S as Vertex of G ;
G .reachableFrom v = the_Vertices_of G by GLIB_002:16;
then ( the Element of S in S & the Element of S in G .reachableFrom v ) ;
then S meets G .reachableFrom v by XBOOLE_0:3;
hence not G .AdjacentSet S is empty by A1, Th43; :: thesis: verum