reconsider L = K as Subfield of K by Th1;
take L ; :: thesis: L is finite
thus L is finite ; :: thesis: verum