{a} c= {a,b}

proof

now :: thesis: for o being object st o in {a} holds
o in {a,b}

let o be object ; :: thesis: ( o in {a} implies o in {a,b} )
assume o in {a} ; :: thesis: o in {a,b}
then o = a by TARSKI:def 1;
hence o in {a,b} by TARSKI:def 2; :: thesis: verum

end;

hence {a} c= {a,b} ; :: thesis: verum

end;

then FAdj (F,{a}) is Subfield of FAdj (F,{a,b}) by FIELD_7:10;
hence FAdj (F,{a,b}) is FAdj (F,{a}) -extending by FIELD_4:7; :: thesis: FAdj (F,{a,b}) is FAdj (F,{b}) -extending
{b} c= {a,b}

proof

now :: thesis: for o being object st o in {b} holds
o in {a,b}

let o be object ; :: thesis: ( o in {b} implies o in {a,b} )
assume o in {b} ; :: thesis: o in {a,b}
then o = b by TARSKI:def 1;
hence o in {a,b} by TARSKI:def 2; :: thesis: verum

end;

hence {b} c= {a,b} ; :: thesis: verum

end;

then FAdj (F,{b}) is Subfield of FAdj (F,{a,b}) by FIELD_7:10;
hence FAdj (F,{a,b}) is FAdj (F,{b}) -extending by FIELD_4:7; :: thesis: verum