1. n : {1...}
2. h : {2..(n+1)}
3. n = {2..n+1}(h)
4. is_prime_factorization(2; (n+1); h)
5. x : Prime
6. n<x
  complete_intseg_mset(2; (n+1); h)(x) = 0

By:	Rewrite by Thm*  a,b:, f:({a..b}), x:. Thm*  a  x < b  complete_intseg_mset(a; b; f)(x) = 0 THEN Analyze

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html