theorem subfie: :: FIELD_12:45

for F, K being Field holds
( K in SubFields F iff K is strict Subfield of F )