let F be Ring; :: thesis: for S being RingExtension of F
for T1, T2 being Subset of S st T1 c= T2 holds
RAdj (F,T1) is Subring of RAdj (F,T2)
let E be RingExtension of F; :: thesis: for T1, T2 being Subset of E st T1 c= T2 holds
RAdj (F,T1) is Subring of RAdj (F,T2)
let T1, T2 be Subset of E; :: thesis: ( T1 c= T2 implies RAdj (F,T1) is Subring of RAdj (F,T2) )
assume AS: T1 c= T2 ; :: thesis: RAdj (F,T1) is Subring of RAdj (F,T2)
H: T2 is Subset of (RAdj (F,T2)) by FIELD_6:30;

now :: thesis: for o being object st o in T1 holds
o in the carrier of (RAdj (F,T2))

let o be object ; :: thesis: ( o in T1 implies o in the carrier of (RAdj (F,T2)) )
assume o in T1 ; :: thesis: o in the carrier of (RAdj (F,T2))
then o in T2 by AS;
hence o in the carrier of (RAdj (F,T2)) by H; :: thesis: verum

end;

then A: T1 c= the carrier of (RAdj (F,T2)) ;
F is Subring of RAdj (F,T2) by FIELD_4:def 1;
hence RAdj (F,T1) is Subring of RAdj (F,T2) by A, FIELD_6:32; :: thesis: verum