let R be Ring; :: thesis: for S being RingExtension of R
for T being Subset of S
for x being Element of (RAdj (R,T)) holds x is Element of S
let S be RingExtension of R; :: thesis: for T being Subset of S
for x being Element of (RAdj (R,T)) holds x is Element of S
let T be Subset of S; :: thesis: for x being Element of (RAdj (R,T)) holds x is Element of S
let x be Element of (RAdj (R,T)); :: thesis: x is Element of S
A1: the carrier of (RAdj (R,T)) = carrierRA T by dRA;
x in the carrier of (RAdj (R,T)) ;
hence x is Element of S by A1; :: thesis: verum