{a,b} c= {a,b,c}

proof

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

let o be object ; :: thesis: ( o in {a,b} implies b₁ in {a,b,c} )
assume o in {a,b} ; :: thesis: b₁ in {a,b,c}

per cases then ( o = a or o = b ) by TARSKI:def 2;

suppose o = a ; :: thesis: b₁ in {a,b,c}

hence o in {a,b,c} by ENUMSET1:def 1; :: thesis: verum

end;

suppose o = b ; :: thesis: b₁ in {a,b,c}

hence o in {a,b,c} by ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

proof

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

let o be object ; :: thesis: ( o in {a,c} implies b₁ in {a,b,c} )
assume o in {a,c} ; :: thesis: b₁ in {a,b,c}

per cases then ( o = a or o = c ) by TARSKI:def 2;

suppose o = a ; :: thesis: b₁ in {a,b,c}

hence o in {a,b,c} by ENUMSET1:def 1; :: thesis: verum

end;

suppose o = c ; :: thesis: b₁ in {a,b,c}

hence o in {a,b,c} by ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

proof

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

let o be object ; :: thesis: ( o in {b,c} implies b₁ in {a,b,c} )
assume o in {b,c} ; :: thesis: b₁ in {a,b,c}

per cases then ( o = b or o = c ) by TARSKI:def 2;

suppose o = b ; :: thesis: b₁ in {a,b,c}

hence o in {a,b,c} by ENUMSET1:def 1; :: thesis: verum

end;

suppose o = c ; :: thesis: b₁ in {a,b,c}

hence o in {a,b,c} by ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

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

end;

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