let n be Nat; :: thesis: n < primenumber n
defpred S₁[ Nat] means $1 < primenumber $1;
A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then A3: n + 1 <= primenumber n by NAT_1:13;
n < n + 1 by NAT_1:13;
then primenumber n < primenumber (n + 1) by MOEBIUS2:21;
hence S₁[n + 1] by A3, XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence n < primenumber n ; :: thesis: verum