let U be Universe; :: thesis: for C being class of U holds not C is finite
let C be class of U; :: thesis: not C is finite
assume A1: C is finite ; :: thesis: contradiction
C is U -Class by Def12;
hence contradiction by A1, Th28; :: thesis: verum