let F be Field; :: thesis: for R being RingExtension of F
for T being Subset of R holds F is Subfield of RAdj (F,T)
let R be RingExtension of F; :: thesis: for T being Subset of R holds F is Subfield of RAdj (F,T)
let T be Subset of R; :: thesis: F is Subfield of RAdj (F,T)
F is Subring of RAdj (F,T) by RAsub;
hence F is Subfield of RAdj (F,T) by defsubfr; :: thesis: verum