let K1, K2 be strict Ring; :: thesis: ( K1 is Subring of K2 & K2 is Subring of K1 implies K1 = K2 )
assume A1: ( K1 is Subring of K2 & K2 is Subring of K1 ) ; :: thesis: K1 = K2
A2: ( the carrier of K1 c= the carrier of K2 & the carrier of K2 c= the carrier of K1 ) by A1, C0SP1:def 3;
then A3: the carrier of K1 = the carrier of K2 by XBOOLE_0:def 10;
A4: the addF of K2 = the addF of K2 || the carrier of K1 by A3
.= the addF of K1 by A1, C0SP1:def 3 ;
A5: the multF of K2 = the multF of K2 || the carrier of K1 by A3
.= the multF of K1 by A1, C0SP1:def 3 ;
( 1. K1 = 1. K2 & 0. K1 = 0. K2 ) by A1, C0SP1:def 3;
hence K1 = K2 by A4, A5, A2, XBOOLE_0:def 10; :: thesis: verum