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 consider t being Vertex of G such that
A1: ( t = x & not t in S & ex v being Vertex of G st
( v in S & t,v are_adjacent ) ) ;
thus not x in S by A1; :: thesis: verum