let p be natural Number ; :: thesis: SetPrimenumber p is finite
SetPrimenumber p c= Seg p by Th70;
hence SetPrimenumber p is finite ; :: thesis: verum