let p be Nat; :: thesis: SetPrimenumber p is finite
SetPrimenumber p c= Seg p by Th84;
hence SetPrimenumber p is finite ; :: thesis: verum