FAdj (F,T1) is Subfield of FAdj (F,(T1 \/ T2)) by XBOOLE_1:7, FIELD_7:10;
hence FAdj (F,(T1 \/ T2)) is FAdj (F,T1) -extending by FIELD_4:7; :: thesis: FAdj (F,(T1 \/ T2)) is FAdj (F,T2) -extending
FAdj (F,T2) is Subfield of FAdj (F,(T1 \/ T2)) by XBOOLE_1:7, FIELD_7:10;
hence FAdj (F,(T1 \/ T2)) is FAdj (F,T2) -extending by FIELD_4:7; :: thesis: verum