take card (SetPrimenumber p) ; :: thesis: primenumber (card (SetPrimenumber p)) = p
p in NAT by ORDINAL1:def 12;
hence primenumber (card (SetPrimenumber p)) = p by A1, NEWTON:def 8; :: thesis: verum