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