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 .order()) +` (G .size())) such that
A1: ( a = c & G is c -tcolorable ) ;
thus a is cardinal number by A1; :: thesis: verum

end;

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