now :: thesis: for x, y being set st x in the_Vertices_of S & y in the_Vertices_of S & x <> y holds
x misses y

let x, y be set ; :: thesis: ( x in the_Vertices_of S & y in the_Vertices_of S & x <> y implies x misses y )
assume x in the_Vertices_of S ; :: thesis: ( y in the_Vertices_of S & x <> y implies x misses y )
then consider G being _Graph such that
A1: ( G in S & x = the_Vertices_of G ) by GLIB_014:def 14;
assume y in the_Vertices_of S ; :: thesis: ( x <> y implies x misses y )
then consider H being _Graph such that
A2: ( H in S & y = the_Vertices_of H ) by GLIB_014:def 14;
assume x <> y ; :: thesis: x misses y
then H <> G by A1, A2;
hence x misses y by A1, A2, Def18; :: thesis: verum

end;

hence the_Vertices_of S is mutually-disjoint by TAXONOM2:def 5; :: thesis: verum