let x be object ; :: thesis: ( x in G .supOutDegree() implies x in G .supDegree() )
assume x in G .supOutDegree() ; :: thesis: x in G .supDegree()
then consider X being set such that
A1: ( x in X & X in { (v .outDegree()) where v is Vertex of G : verum } ) by TARSKI:def 4;
consider v being Vertex of G such that
A2: X = v .outDegree() by A1;
v .outDegree() c= v .degree() by CARD_2:94;
then A3: x in v .degree() by A1, A2;
v .degree() in { (w .degree()) where w is Vertex of G : verum } ;
hence x in G .supDegree() by A3, TARSKI:def 4; :: thesis: verum