consider e being object such that
A5:
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 v = (the_Source_of G) . e as Vertex of G by A5, FUNCT_2:5;
e in v .edgesOut()
by A5, GLIB_000:58;
then
( v .outDegree() <> 0 & 0 c= v .outDegree() )
by XBOOLE_1:2;
then A6:
0 in v .outDegree()
by XBOOLE_0:def 8, ORDINAL1:11;
v .outDegree() in { (u .outDegree()) where u is Vertex of G : verum }
;
then
v .outDegree() c= G .supOutDegree()
by ZFMISC_1:74;
hence
not G .supOutDegree() is empty
by A6; verum