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

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

end;

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