now :: thesis: for a being set st a in H₂(G) holds
a is cardinal number

let a be set ; :: thesis: ( a in H₂(G) implies a is cardinal number )
assume a in H₂(G) ; :: thesis: a is cardinal number
then consider c being cardinal Subset of (G .size()) such that
A1: ( a = c & G is c -ecolorable ) ;
thus a is cardinal number by A1; :: thesis: verum

end;

hence meet { c where c is cardinal Subset of (G .size()) : G is c -ecolorable } is Cardinal by GLIBPRE0:15; :: thesis: verum