let p be Prime; :: thesis: primeindex p < p
primeindex p < primenumber (primeindex p) by Th10;
hence primeindex p < p by NUMBER10:def 4; :: thesis: verum