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