1. r : 
2. s : 
3. CoPrime(r,s)
4. a : 
5. b : 
  x:. (x = a mod r) & (x = b mod s)

By:	(Inst Thm* r,s:. CoPrime(r,s)  (x:. (x = 1 mod r) & (x = 0 mod s)) [r;s]) THEN (Inst Thm* r,s:. CoPrime(r,s)  (x:. (x = 1 mod r) & (x = 0 mod s)) [s;r])

1	6. x:. (x = 1 mod r) & (x = 0 mod s)   CoPrime(s,r)	2 steps
2	6. x:. (x = 1 mod r) & (x = 0 mod s) 7. x:. (x = 1 mod s) & (x = 0 mod r)   x:. (x = a mod r) & (x = b mod s)	6 steps

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