let K be Field; :: thesis: for SK1, SK2 being strict Subfield of K holds
( SK1 = SK2 iff the carrier of SK1 = the carrier of SK2 )
let SK1, SK2 be strict Subfield of K; :: thesis: ( SK1 = SK2 iff the carrier of SK1 = the carrier of SK2 )
thus ( SK1 = SK2 implies the carrier of SK1 = the carrier of SK2 ) ; :: thesis: ( the carrier of SK1 = the carrier of SK2 implies SK1 = SK2 )
assume A1: the carrier of SK1 = the carrier of SK2 ; :: thesis: SK1 = SK2
then A2: SK2 is strict Subfield of SK1 by Th6;
SK1 is strict Subfield of SK2 by A1, Th6;
hence SK1 = SK2 by A2, Th4; :: thesis: verum