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

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

end;

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