now :: thesis: for d being set st d in { (v .outDegree()) where v is Vertex of G : verum } holds
d c= G .size()

let d be set ; :: thesis: ( d in { (v .outDegree()) where v is Vertex of G : verum } implies d c= G .size() )
assume d in { (v .outDegree()) where v is Vertex of G : verum } ; :: thesis: d c= G .size()
then consider v being Vertex of G such that
A3: d = v .outDegree() ;
thus d c= G .size() by A3, CARD_1:11; :: thesis: verum

end;

then G .supOutDegree() c= G .size() by ZFMISC_1:76;
hence G .supOutDegree() is natural ; :: thesis: verum