assume not union (the_Edges_of S) is empty ; :: thesis: contradiction
then consider e being object such that
A1: e in union (the_Edges_of S) by XBOOLE_0:def 1;
consider E being set such that
A2: ( e in E & E in the_Edges_of S ) by A1, TARSKI:def 4;
consider G being _Graph such that
A3: ( G in S & E = the_Edges_of G ) by A2, Def15;
e in the_Edges_of G by A2, A3;
hence contradiction by A3; :: thesis: verum