theorem :: EC_PF_1:5

for K1, K2, K3 being Field st K1 is Subfield of K2 & K2 is Subfield of K3 holds
K1 is Subfield of K3