IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime factorization includes prime divisors a:, b:, f:({a..b}), p:.
is_prime_factorization(a; b; f)
prime(p) p | {a..b}(f) p {a..b} & 0<f(p)
By:
IntroduceGuardForms (<prop> & <prop>) 0
THEN
Def of {<int>..<int>}(<exponents>) ...