assume not the_Edges_of S is empty ; :: thesis: contradiction
then consider E being object such that
A2: E in the_Edges_of S by XBOOLE_0:def 1;
ex G being _Graph st
( G in S & E = the_Edges_of G ) by A2, Def15;
hence contradiction ; :: thesis: verum