consider e being object such that
A1: 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 A1, FUNCT_2:5;
e in v .edgesOut() by A1, GLIB_000:58;
then ( v .outDegree() <> 0 & 0 c= v .outDegree() ) by XBOOLE_1:2;
then 0 in v .outDegree() by XBOOLE_0:def 8, ORDINAL1:11;
then A2: 0 in v .degree() by CARD_2:94, TARSKI:def 3;
v .degree() in { (u .degree()) where u is Vertex of G : verum } ;
then v .degree() c= G .supDegree() by ZFMISC_1:74;
hence not G .supDegree() is empty by A2; :: thesis: verum