set X = { u where u is Vertex of G : ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) } ;

now :: thesis: for x being object st x in { u where u is Vertex of G : ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) } holds
x in the_Vertices_of G

let x be object ; :: thesis: ( x in { u where u is Vertex of G : ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) } implies x in the_Vertices_of G )
assume x in { u where u is Vertex of G : ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) } ; :: thesis: x in the_Vertices_of G
then ex u being Vertex of G st
( u = x & not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) ;
hence x in the_Vertices_of G ; :: thesis: verum

end;

hence { u where u is Vertex of G : ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) } is Subset of (the_Vertices_of G) by TARSKI:def 3; :: thesis: verum