let F, K be Field; :: thesis: ( K in SubFields F iff K is strict Subfield of F )

now :: thesis: ( K in SubFields F implies K is strict Subfield of F )

assume K in SubFields F ; :: thesis: K is strict Subfield of F
then consider K1 being strict Field such that
B: ( K1 = K & K1 is Subfield of F ) by defX;
thus K is strict Subfield of F by B; :: thesis: verum

end;

hence ( K in SubFields F iff K is strict Subfield of F ) by defX; :: thesis: verum