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
A2: x = v .inDegree() ;
thus x is cardinal number by A2; :: thesis: verum

end;

hence union { (v .inDegree()) where v is Vertex of G : verum } is Cardinal by TOPGEN_2:3; :: thesis: verum