let G be _Graph; :: thesis: for S, x being set st x in G .AdjacentSet S holds

not x in S

let S, x be set ; :: thesis: ( x in G .AdjacentSet S implies not x in S )

assume x in G .AdjacentSet S ; :: thesis: not x in S

then ex t being Vertex of G st

( t = x & not t in S & ex v being Vertex of G st

( v in S & t,v are_adjacent ) ) ;

hence not x in S ; :: thesis: verum

not x in S

let S, x be set ; :: thesis: ( x in G .AdjacentSet S implies not x in S )

assume x in G .AdjacentSet S ; :: thesis: not x in S

then ex t being Vertex of G st

( t = x & not t in S & ex v being Vertex of G st

( v in S & t,v are_adjacent ) ) ;

hence not x in S ; :: thesis: verum