let K be Field; :: thesis: for SK1, SK2 being strict Subfield of K holds
( SK1 = SK2 iff for x being set holds
( x in SK1 iff x in SK2 ) )
let SK1, SK2 be strict Subfield of K; :: thesis: ( SK1 = SK2 iff for x being set holds
( x in SK1 iff x in SK2 ) )
thus ( SK1 = SK2 implies for x being set holds
( x in SK1 iff x in SK2 ) ) ; :: thesis: ( ( for x being set holds
( x in SK1 iff x in SK2 ) ) implies SK1 = SK2 )
assume for x being set holds
( x in SK1 iff x in SK2 ) ; :: thesis: SK1 = SK2
then ( SK1 is strict Subfield of SK2 & SK2 is strict Subfield of SK1 ) by Th7;
hence SK1 = SK2 by Th4; :: thesis: verum