let R be Ring; :: thesis: for S being RingExtension of R
for T being Subset of S holds R is Subring of RAdj (R,T)
let S be RingExtension of R; :: thesis: for T being Subset of S holds R is Subring of RAdj (R,T)
let T be Subset of S; :: thesis: R is Subring of RAdj (R,T)
set P = RAdj (R,T);
X: R is Subring of S by FIELD_4:def 1;
A: 1. (RAdj (R,T)) = 1. S by dRA
.= 1. R by X, C0SP1:def 3 ;
B: 0. (RAdj (R,T)) = 0. S by dRA
.= 0. R by X, C0SP1:def 3 ;
C: the carrier of R c= the carrier of (RAdj (R,T))

proof

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

let o be object ; :: thesis: ( o in the carrier of R implies o in the carrier of (RAdj (R,T)) )
assume C1: o in the carrier of R ; :: thesis: o in the carrier of (RAdj (R,T))
the carrier of R c= the carrier of S by X, C0SP1:def 3;
then reconsider a = o as Element of S by C1;

now :: thesis: for U being Subring of S st R is Subring of U & T is Subset of U holds
o in U

let U be Subring of S; :: thesis: ( R is Subring of U & T is Subset of U implies o in U )
assume ( R is Subring of U & T is Subset of U ) ; :: thesis: o in U
then the carrier of R c= the carrier of U by C0SP1:def 3;
hence o in U by C1; :: thesis: verum

end;

then a in carrierRA T ;
hence o in the carrier of (RAdj (R,T)) by dRA; :: thesis: verum

end;

hence the carrier of R c= the carrier of (RAdj (R,T)) ; :: thesis: verum

end;

then Y: [: the carrier of R, the carrier of R:] c= [: the carrier of (RAdj (R,T)), the carrier of (RAdj (R,T)):] by ZFMISC_1:96;
D: the addF of (RAdj (R,T)) || the carrier of R = ( the addF of S || (carrierRA T)) || the carrier of R by dRA
.= ( the addF of S || the carrier of (RAdj (R,T))) || the carrier of R by dRA
.= the addF of S || the carrier of R by Y, FUNCT_1:51
.= the addF of R by X, C0SP1:def 3 ;
the multF of (RAdj (R,T)) || the carrier of R = ( the multF of S || (carrierRA T)) || the carrier of R by dRA
.= ( the multF of S || the carrier of (RAdj (R,T))) || the carrier of R by dRA
.= the multF of S || the carrier of R by Y, FUNCT_1:51
.= the multF of R by X, C0SP1:def 3 ;
hence R is Subring of RAdj (R,T) by A, B, C, D, C0SP1:def 3; :: thesis: verum