assume not the_Target_of S is empty ; :: thesis: contradiction
then consider t being object such that
A4: t in the_Target_of S by XBOOLE_0:def 1;
ex G being _Graph st
( G in S & t = the_Target_of G ) by A4, Def17;
hence contradiction ; :: thesis: verum