S-K basis Completeness in combinatory logic

Question

I was reading the following Wikipedia page on combinatory logic and am puzzled by the example that is given:
https://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis
Using the given transformation T[], the term λx.λy.(y x) is converted to a SKI combinator.

Here is the first rewriting step:

T[λx.λy.(y x)]
= T[λx.T[λy.(y x)]] (by 5)

Where 5. is:
T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)

I am failing to understand why 5. is being used here. In λx.λy.(y x), isn't x a bound variable (meaning it doesn't occur free in E)?

Answer 1

In λx.λy.(y x), x is a bound variable and is thus not free. But in y x, x is free. The proviso of the rule refers to E without the lambdas around it.