theorem FAt: :: FIELD_6:35

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