is automatically a Finitely generated field extension, so for some . Applying ^P1 and iterating on ^P1 and ^P2, we have

proving the inequality.

To show ^S1 implies ^S3: If are separable over , then they are separable over all algebraic extensions, so equality follows by ^P1.

To show ^S3 implies ^S2: Suppose , and for some consider the intermediate extension . By ^P2, we have

which can only hold (by the inequality of ^P1) if in particular

Therefore, again by ^P1, every is separable, whence by definition is separable.

That ^S2 implies ^S1 is clear, since a finite extension is finitely generated.