for K1, K2 being Field st K1 is Subfield of K2 holds
for x being set st x in K1 holds
x in K2