let R be Field; :: thesis: for E being FieldExtension of R
for T being Subset of E holds T is Subset of (FAdj (R,T))
let S be FieldExtension of R; :: thesis: for T being Subset of S holds T is Subset of (FAdj (R,T))
let T be Subset of S; :: thesis: T is Subset of (FAdj (R,T))
set P = FAdj (R,T);
now :: thesis: for o being object st o in T holds
o in the carrier of (FAdj (R,T))
let o be object ; :: thesis: ( o in T implies o in the carrier of (FAdj (R,T)) )
assume A: o in T ; :: thesis: o in the carrier of (FAdj (R,T))
then reconsider a = o as Element of S ;
for U being Subfield of S st R is Subfield of U & T is Subset of U holds
o in U by A;
then a in carrierFA T ;
hence o in the carrier of (FAdj (R,T)) by dFA; :: thesis: verum
end;
hence T is Subset of (FAdj (R,T)) by TARSKI:def 3; :: thesis: verum