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 A0: the carrier of K1 c= the carrier of K2 by PFDef2;
for x being set st x in K1 holds
x in K2

proof

let x be set ; :: thesis: ( x in K1 implies x in K2 )
assume x in K1 ; :: thesis: x in K2
then x in the carrier of K1 by STRUCT_0:def 5;
hence x in K2 by A0, STRUCT_0:def 5; :: thesis: verum

end;

hence for x being set st x in K1 holds
x in K2 ; :: thesis: verum