now :: thesis: ( F1 == F2 implies ( F1 is Subfield of F2 & F2 is Subfield of F1 ) )

assume F1 == F2 ; :: thesis: ( F1 is Subfield of F2 & F2 is Subfield of F1 )
then A: ( the carrier of F1 = the carrier of F2 & the addF of F1 = the addF of F2 || the carrier of F1 & the multF of F1 = the multF of F2 || the carrier of F1 & 1. F1 = 1. F2 & 0. F1 = 0. F2 ) ;
hence F1 is Subfield of F2 by EC_PF_1:def 1; :: thesis: F2 is Subfield of F1
thus F2 is Subfield of F1 by A, EC_PF_1:def 1; :: thesis: verum

end;

hence ( F1 == F2 iff ( F1 is Subfield of F2 & F2 is Subfield of F1 ) ) by Th0; :: thesis: verum