let F be Field; :: thesis: for K being Subfield of F holds carrier/\ F c= the carrier of K
let K be Subfield of F; :: thesis: carrier/\ F c= the carrier of K

now :: thesis: for x being object st x in carrier/\ F holds
x in the carrier of K

let x be object ; :: thesis: ( x in carrier/\ F implies x in the carrier of K )
assume x in carrier/\ F ; :: thesis: x in the carrier of K
then consider y being Element of F such that
A1: ( x = y & ( for E being Subfield of F holds y in E ) ) ;
y in K by A1;
hence x in the carrier of K by A1; :: thesis: verum

end;

hence carrier/\ F c= the carrier of K ; :: thesis: verum