let X be set ; :: thesis: ( X = the_Vertices_of S iff X = { (the_Vertices_of G) where G is Element of S : verum } )
set Y = { (the_Vertices_of G) where G is Element of S : verum } ;

now :: thesis: for V being object holds
( ( V in the_Vertices_of S implies V in { (the_Vertices_of G) where G is Element of S : verum } ) & ( V in { (the_Vertices_of G) where G is Element of S : verum } implies V in the_Vertices_of S ) )

let V be object ; :: thesis: ( ( V in the_Vertices_of S implies V in { (the_Vertices_of G) where G is Element of S : verum } ) & ( V in { (the_Vertices_of G) where G is Element of S : verum } implies V in the_Vertices_of S ) )

hereby :: thesis: ( V in { (the_Vertices_of G) where G is Element of S : verum } implies V in the_Vertices_of S )

assume V in the_Vertices_of S ; :: thesis: V in { (the_Vertices_of G) where G is Element of S : verum }
then ex G being _Graph st
( G in S & V = the_Vertices_of G ) by Def14;
hence V in { (the_Vertices_of G) where G is Element of S : verum } ; :: thesis: verum

end;

assume V in { (the_Vertices_of G) where G is Element of S : verum } ; :: thesis: V in the_Vertices_of S
then consider G being Element of S such that
A1: V = the_Vertices_of G ;
thus V in the_Vertices_of S by A1, Def14; :: thesis: verum

end;

hence ( X = the_Vertices_of S iff X = { (the_Vertices_of G) where G is Element of S : verum } ) by TARSKI:2; :: thesis: verum