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