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

proof

per cases ( f < g or g < f ) by A18, XXREAL_0:1;

case A19: f < g ; :: thesis: n + 1 <= n

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: verum

end;

case A21: g < f ; :: thesis: n + 1 <= n

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: verum

end;

end;

end;

hence contradiction by NAT_1:13; :: thesis: verum