let K be Field; :: thesis: for SK1, SK2 being Subfield of K holds
( SK1 is Subfield of SK2 iff for x being set st x in SK1 holds
x in SK2 )
let SK1, SK2 be Subfield of K; :: thesis: ( SK1 is Subfield of SK2 iff for x being set st x in SK1 holds
x in SK2 )
thus ( SK1 is Subfield of SK2 implies for x being set st x in SK1 holds
x in SK2 ) by Th3; :: thesis: ( ( for x being set st x in SK1 holds
x in SK2 ) implies SK1 is Subfield of SK2 )
assume A1: for x being set st x in SK1 holds
x in SK2 ; :: thesis: SK1 is Subfield of SK2
the carrier of SK1 c= the carrier of SK2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of SK1 or x in the carrier of SK2 )
assume x in the carrier of SK1 ; :: thesis: x in the carrier of SK2
then reconsider x = x as Element of SK1 ;
x in SK1 ;
then x in SK2 by A1;
hence x in the carrier of SK2 ; :: thesis: verum
end;
hence SK1 is Subfield of SK2 by Th6; :: thesis: verum