Generally a Galois extension is defined to be an algebraic extension that is also normal & separable. It is then shown that in the sequence of field extensions $L|M|K$ if $L|K$ is Galois then $L|M$ is. This follows since the same property is valid for separable & normal extensions individually. It also follows that $L|K$ is a Galois extension iff the set of elements of $L$ invariant under the action of $Aut_K L$ is $K$
In Robalo Delgados thesis on Galois Categories referenced in nLab-Grothendiecks Galois Theory he takes the opposite tack, and in definition 22.214.171.124 defines an algebraic extension of fields $L|K$ to be a Galois extension iff the set of elements of $L$ invariant under the action of $Aut_K L$ is $K$.
It is then shown that in the sequence of algebraic field extensions $L|M|K$ if $L|K$ is Galois then $L|M$ is. This is asserted to be an obvious deduction (and so has no details), I don't see the obviousness...can someone clarify.
In proposition 126.96.36.199 he shows that Galois extension is normal and separable.
All this appears to be in the opposite order of the standard treatments. One reason I'm interested in his formulation, if it is correct, is that one side of the Galois correspondence follows easily from this.
disclaimer: I've already asked this question on math.stackexchange but the answers there revolved around characterising Galois extensions as being normal & separable, and then showing this property follows.