let F be Field; :: thesis: for E being FieldExtension of F
for T1, T2 being Subset of E st T1 c= T2 holds
FAdj (F,T1) is Subfield of FAdj (F,T2)
let E be FieldExtension of F; :: thesis: for T1, T2 being Subset of E st T1 c= T2 holds
FAdj (F,T1) is Subfield of FAdj (F,T2)
let T1, T2 be Subset of E; :: thesis: ( T1 c= T2 implies FAdj (F,T1) is Subfield of FAdj (F,T2) )
assume AS: T1 c= T2 ; :: thesis: FAdj (F,T1) is Subfield of FAdj (F,T2)
X: T2 is Subset of (FAdj (F,T2)) by FIELD_6:35;

now :: thesis: for o being object st o in T1 holds
o in the carrier of (FAdj (F,T2))

let o be object ; :: thesis: ( o in T1 implies o in the carrier of (FAdj (F,T2)) )
assume o in T1 ; :: thesis: o in the carrier of (FAdj (F,T2))
then o in T2 by AS;
hence o in the carrier of (FAdj (F,T2)) by X; :: thesis: verum

end;

then A: T1 c= the carrier of (FAdj (F,T2)) ;
F is Subfield of FAdj (F,T2) by FIELD_4:7;
hence FAdj (F,T1) is Subfield of FAdj (F,T2) by A, FIELD_6:37; :: thesis: verum