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