assume not the_Source_of S is empty ; :: thesis: contradiction
then consider s being object such that
A3: s in the_Source_of S by XBOOLE_0:def 1;
ex G being _Graph st
( G in S & s = the_Source_of G ) by A3, Def16;
hence contradiction ; :: thesis: verum