consider e being object such that
A3: e in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G) . e;
set w = (the_Target_of G) . e;
reconsider w = (the_Target_of G) . e as Vertex of G by A3, FUNCT_2:5;
e in w .edgesIn() by A3, GLIB_000:56;
then ( w .inDegree() <> 0 & 0 c= w .inDegree() ) by XBOOLE_1:2;
then A4: 0 in w .inDegree() by XBOOLE_0:def 8, ORDINAL1:11;
w .inDegree() in { (u .inDegree()) where u is Vertex of G : verum } ;
then w .inDegree() c= G .supInDegree() by ZFMISC_1:74;
hence not G .supInDegree() is empty by A4; :: thesis: verum