ex E being Field st E is Subring of RAdj (F,T)

proof

take F ; :: thesis: F is Subring of RAdj (F,T)
thus F is Subring of RAdj (F,T) by RAsub; :: thesis: verum

end;

hence RAdj (F,T) is field-containing ; :: thesis: verum