let K1, K2 be strict Field; :: thesis: ( K1 is Subfield of K2 & K2 is Subfield of K1 implies K1 = K2 )
assume AS: ( K1 is Subfield of K2 & K2 is Subfield of K1 ) ; :: thesis: K1 = K2
P3: ( the carrier of K1 c= the carrier of K2 & the carrier of K2 c= the carrier of K1 ) by AS, PFDef2;
then P0: the carrier of K1 = the carrier of K2 by XBOOLE_0:def 10;
P1: the addF of K2 = the addF of K2 || the carrier of K1 by P0, RELSET_1:19
.= the addF of K1 by AS, PFDef2 ;
P2: the multF of K2 = the multF of K2 || the carrier of K1 by P0, RELSET_1:19
.= the multF of K1 by AS, PFDef2 ;
( 1. K1 = 1. K2 & 0. K1 = 0. K2 ) by AS, PFDef2;
hence K1 = K2 by P1, P2, P3, XBOOLE_0:def 10; :: thesis: verum