A: F is Subfield of E by FIELD_4:7;
E is Subfield of E by FIELD_4:1;
hence FieldAdjunction (F,T) is strict Subfield of E by A, FAsub2; :: thesis: verum