let f, g be prime Element of NAT ; :: thesis:
assume that
A16: n = card (SetPrimenumber f) and
A17: n = card (SetPrimenumber g) ; :: thesis:
assume A18: f <> g ; :: thesis:
( ( f < g & n + 1 <= n ) or ( g < f & n + 1 <= n ) )

per cases by A18, XXREAL_0:1;

case A19: f < g ; :: thesis:

A20: not f in SetPrimenumber f by Def7;
card ((SetPrimenumber f) \/ {f}) <= card (SetPrimenumber g) by A19, Th76, NAT_1:43;
hence n + 1 <= n by A16, A17, A20, CARD_2:41; :: thesis:

end;

case A21: g < f ; :: thesis:

A22: not g in SetPrimenumber g by Def7;
card ((SetPrimenumber g) \/ {g}) <= card (SetPrimenumber f) by A21, Th76, NAT_1:43;
hence n + 1 <= n by A16, A17, A22, CARD_2:41; :: thesis:

end;

end;

end;

hence contradiction by NAT_1:13; :: thesis: