theorem Th1: :: FIELD_7:3

for F being Field
for E being FieldExtension of F
for T being Subset of E holds
( FAdj (F,T) == F iff T is Subset of F )