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: u in G .AdjacentSet S
thus u in G .AdjacentSet S by A1, A2; :: thesis: verum