now :: thesis: for x being set st x in { (v .degree()) where v is Vertex of G : verum } holds
x is cardinal number
let x be set ; :: thesis: ( x in { (v .degree()) where v is Vertex of G : verum } implies x is cardinal number )
assume x in { (v .degree()) where v is Vertex of G : verum } ; :: thesis: x is cardinal number
then consider v being Vertex of G such that
A4: x = v .degree() ;
thus x is cardinal number by A4; :: thesis: verum
end;
hence meet { (v .degree()) where v is Vertex of G : verum } is Cardinal by GLIBPRE0:15; :: thesis: verum