let R be Ring; :: thesis: for S being RingExtension of R
for T being Subset of S holds T is Subset of (RAdj (R,T))
let S be RingExtension of R; :: thesis: for T being Subset of S holds T is Subset of (RAdj (R,T))
let T be Subset of S; :: thesis: T is Subset of (RAdj (R,T))
set P = RAdj (R,T);

now :: thesis: for o being object st o in T holds
o in the carrier of (RAdj (R,T))

let o be object ; :: thesis: ( o in T implies o in the carrier of (RAdj (R,T)) )
assume A: o in T ; :: thesis: o in the carrier of (RAdj (R,T))
then reconsider a = o as Element of S ;
for U being Subring of S st R is Subring of U & T is Subset of U holds
o in U by A;
then a in carrierRA T ;
hence o in the carrier of (RAdj (R,T)) by dRA; :: thesis: verum

end;

hence T is Subset of (RAdj (R,T)) by TARSKI:def 3; :: thesis: verum