theorem :: EC_PF_1:9

for K being Field
for SK1, SK2 being strict Subfield of K holds
( SK1 = SK2 iff for x being set holds
( x in SK1 iff x in SK2 ) )