let F1, F2 be Field; :: thesis: ( F1 is Subfield of F2 & F2 is Subfield of F1 implies F1 == F2 )
assume AS1: ( F1 is Subfield of F2 & F2 is Subfield of F1 ) ; :: thesis: F1 == F2
then B: ( 1. F1 = 1. F2 & 0. F1 = 0. F2 ) by EC_PF_1:def 1;
A: ( the carrier of F1 c= the carrier of F2 & the carrier of F2 c= the carrier of F1 ) by AS1, EC_PF_1:def 1;
then E: the carrier of F2 = the carrier of F1 by TARSKI:2;
C: the addF of F1 = the addF of F2 || the carrier of F1 by AS1, EC_PF_1:def 1
.= the addF of F2 by E ;
the multF of F1 = the multF of F2 || the carrier of F1 by AS1, EC_PF_1:def 1
.= the multF of F2 by E ;
hence F1 == F2 by A, B, C, TARSKI:2; :: thesis: verum