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 ) ) )

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

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 that ( 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;( 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

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