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 ) ) } ;

( v in S & u,v are_adjacent ) ) } is Subset of (the_Vertices_of G) by TARSKI:def 3; :: thesis: verum

( 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

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 ) ) } 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;( 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

( v in S & u,v are_adjacent ) ) } is Subset of (the_Vertices_of G) by TARSKI:def 3; :: thesis: verum