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

let x be set ; :: 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 A1: 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
consider u being Vertex of G such that
A2: u = x and
( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) by A1;
thus x in the_Vertices_of G by A2; :: 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