%lemmaE8

lemmaE8(S,T,X) == ((eta(S,T) and eta(S,X))
                  => exists(Z,((Z=T or eta(T,Z)) and (Z=X or eta(X,Z))))).