let K1, K2 be strict Field; :: thesis: ( K1 is Subfield of K2 & K2 is Subfield of K1 implies K1 = K2 )
assume A1: ( K1 is Subfield of K2 & K2 is Subfield 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, Def1;
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, RELSET_1:19
.= the addF of K1 by A1, Def1 ;
A5: the multF of K2 = the multF of K2 || the carrier of K1 by A3, RELSET_1:19
.= the multF of K1 by A1, Def1 ;
( 1. K1 = 1. K2 & 0. K1 = 0. K2 ) by A1, Def1;
hence K1 = K2 by A4, A5, A2, XBOOLE_0:def 10; :: thesis: verum