let K be Ring; :: thesis: for R1, R2 being Subring of K holds
( R1 is Subring of R2 iff the carrier of R1 c= the carrier of R2 )
let SK1, SK2 be Subring of K; :: thesis: ( SK1 is Subring of SK2 iff the carrier of SK1 c= the carrier of SK2 )
set C1 = the carrier of SK1;
set C2 = the carrier of SK2;
set ADD = the addF of K;
set MULT = the multF of K;
thus ( SK1 is Subring of SK2 implies the carrier of SK1 c= the carrier of SK2 ) by C0SP1:def 3; :: thesis: ( the carrier of SK1 c= the carrier of SK2 implies SK1 is Subring of SK2 )
assume A1: the carrier of SK1 c= the carrier of SK2 ; :: thesis: SK1 is Subring of SK2
then A2: [: the carrier of SK1, the carrier of SK1:] c= [: the carrier of SK2, the carrier of SK2:] by ZFMISC_1:96;
the addF of SK2 = the addF of K || the carrier of SK2 by C0SP1:def 3;
then A3: the addF of SK2 || the carrier of SK1 = the addF of K || the carrier of SK1 by A2, FUNCT_1:51
.= the addF of SK1 by C0SP1:def 3 ;
the multF of SK2 = the multF of K || the carrier of SK2 by C0SP1:def 3;
then A4: the multF of SK2 || the carrier of SK1 = the multF of K || the carrier of SK1 by A2, FUNCT_1:51
.= the multF of SK1 by C0SP1:def 3 ;
( 1. SK1 = 1. K & 0. SK1 = 0. K ) by C0SP1:def 3;
then ( 1. SK1 = 1. SK2 & 0. SK1 = 0. SK2 ) by C0SP1:def 3;
hence SK1 is Subring of SK2 by A1, A3, A4, C0SP1:def 3; :: thesis: verum