let R be Ring; :: thesis: for S being RingExtension of R
for T being Subset of S holds
( RAdj (R,T) == R iff T is Subset of R )
let S be RingExtension of R; :: thesis: for T being Subset of S holds
( RAdj (R,T) == R iff T is Subset of R )
let T be Subset of S; :: thesis: ( RAdj (R,T) == R iff T is Subset of R )
set P = RAdj (R,T);
X0: R is Subring of S by FIELD_4:def 1;
X1: R is Subring of R by LIOUVIL2:18;

Z: 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 X0, 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 FIELD_6:def 4; :: thesis: verum

end;

G: now :: thesis: ( T is Subset of R implies RAdj (R,T) == R )

assume B0: T is Subset of R ; :: thesis: RAdj (R,T) == R

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

let o be object ; :: thesis: ( o in the carrier of (RAdj (R,T)) implies o in the carrier of R )
assume o in the carrier of (RAdj (R,T)) ; :: thesis: o in the carrier of R
then o in carrierRA T by FIELD_6:def 4;
then consider x being Element of S such that
B1: ( x = o & ( for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U ) ) ;
x in R by X0, X1, B0, B1;
hence o in the carrier of R by B1; :: thesis: verum

end;

then B1: the carrier of R = the carrier of (RAdj (R,T)) by Z, TARSKI:2;
B2: 1. (RAdj (R,T)) = 1. S by FIELD_6:def 4
.= 1. R by X0, C0SP1:def 3 ;
B3: 0. (RAdj (R,T)) = 0. S by FIELD_6:def 4
.= 0. R by X0, C0SP1:def 3 ;
B4: the addF of (RAdj (R,T)) = the addF of S || (carrierRA T) by FIELD_6:def 4
.= the addF of S || the carrier of R by B1, FIELD_6:def 4
.= the addF of R || the carrier of R by X0, C0SP1:def 3 ;
the multF of (RAdj (R,T)) = the multF of S || (carrierRA T) by FIELD_6:def 4
.= the multF of S || the carrier of R by B1, FIELD_6:def 4
.= the multF of R || the carrier of R by X0, C0SP1:def 3 ;
hence RAdj (R,T) == R by B1, B2, B3, B4, FIELD_7:def 1; :: thesis: verum

end;

now :: thesis: ( RAdj (R,T) == R implies T is Subset of R )

assume RAdj (R,T) == R ; :: thesis: T is Subset of R
then doubleLoopStr(# the carrier of (RAdj (R,T)), the addF of (RAdj (R,T)), the multF of (RAdj (R,T)), the OneF of (RAdj (R,T)), the ZeroF of (RAdj (R,T)) #) = doubleLoopStr(# the carrier of R, the addF of R, the multF of R, the OneF of R, the ZeroF of R #) by FIELD_7:def 1;
hence T is Subset of R by FIELD_6:30; :: thesis: verum

end;

hence ( RAdj (R,T) == R iff T is Subset of R ) by G; :: thesis: verum