per cases ( S is empty or not S is empty ) ;

suppose A1: S is empty ; :: thesis: ex b₁ being set st
for V being object holds
( V in b₁ iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) )

take the empty set ; :: thesis: for V being object holds
( V in the empty set iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) )
thus for V being object holds
( V in the empty set iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) ) by A1; :: thesis: verum

end;

suppose not S is empty ; :: thesis: ex b₁ being set st
for V being object holds
( V in b₁ iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) )

then reconsider S0 = S as non empty Graph-membered set ;
take X = { (the_Vertices_of G) where G is Element of S0 : verum } ; :: thesis: for V being object holds
( V in X iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) )
let V be object ; :: thesis: ( V in X iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) )

hereby :: thesis: ( ex G being _Graph st
( G in S & V = the_Vertices_of G ) implies V in X )

assume V in X ; :: thesis: ex G being _Graph st
( G in S & V = the_Vertices_of G )
then consider G being Element of S0 such that
A2: V = the_Vertices_of G ;
reconsider G = G as _Graph ;
take G = G; :: thesis: ( G in S & V = the_Vertices_of G )
thus ( G in S & V = the_Vertices_of G ) by A2; :: thesis: verum

end;

thus ( ex G being _Graph st
( G in S & V = the_Vertices_of G ) implies V in X ) ; :: thesis: verum

end;

end;