now :: thesis: for x being set st x in { (v .outDegree()) where v is Vertex of G : verum } holds
x is cardinal number

let x be set ; :: thesis: ( x in { (v .outDegree()) where v is Vertex of G : verum } implies x is cardinal number )
assume x in { (v .outDegree()) where v is Vertex of G : verum } ; :: thesis: x is cardinal number
then consider v being Vertex of G such that
A6: x = v .outDegree() ;
thus x is cardinal number by A6; :: thesis: verum

end;

hence meet { (v .outDegree()) where v is Vertex of G : verum } is Cardinal by GLIBPRE0:15; :: thesis: verum