theorem Th1: :: EC_PF_1:1

for K being Field holds K is Subfield of K