let K1, K2 be Field; :: thesis: ( K1 is Subfield of K2 implies for x being set st x in K1 holds
x in K2 )
assume K1 is Subfield of K2 ; :: thesis: for x being set st x in K1 holds
x in K2
then A1: the carrier of K1 c= the carrier of K2 by Def1;
for x being set st x in K1 holds
x in K2 by A1;
hence for x being set st x in K1 holds
x in K2 ; :: thesis: verum