:: deftheorem IS defines inducing_subfield FIELD_16:def 2 :
for F being Field
for S being Subset of F holds
( S is inducing_subfield iff ( 0. F in S & 1. F in S & ( for a, b being Element of F st a in S & b in S holds
( a + b in S & a * b in S & - a in S ) ) & ( for a being non zero Element of F st a in S holds
a " in S ) ) );