let n be Nat; :: thesis: indexp n <= n
card (SetPrimes n) <= card (Seg n) by NAT_1:43, XBOOLE_1:17;
hence indexp n <= n ; :: thesis: verum