let UN be Universe; :: thesis: UN is infinite
A1: omega c= UN by Th16;
assume UN is finite ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum