let G be _Graph; :: thesis: for S being set
for u being Vertex of G holds
( u in G .AdjacentSet S iff ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) )

let S be set ; :: thesis: for u being Vertex of G holds
( u in G .AdjacentSet S iff ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) )

let u be Vertex of G; :: thesis: ( u in G .AdjacentSet S iff ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) )

hereby :: thesis: ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) implies u in G .AdjacentSet S )
assume u in G .AdjacentSet S ; :: thesis: ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) )

then ex t being Vertex of G st
( u = t & not t in S & ex v being Vertex of G st
( v in S & t,v are_adjacent ) ) ;
hence ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) ; :: thesis: verum
end;
assume that
A1: not u in S and
A2: ex v being Vertex of G st
( v in S & u,v are_adjacent ) ; :: thesis:
thus u in G .AdjacentSet S by A1, A2; :: thesis: verum