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

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

end;

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