1. x : 
2. y : 
3. z : 
  x.numy.den=y.numx.den
  
  y.numz.den=z.numy.den  x.numz.den=z.numx.den

By:	RWH (LemmaC Thm* x,y:. x=y  x = y) 0

1

x.numy.den = y.numx.den      y.numz.den = z.numy.den  x.numz.den = z.numx.den

14 steps

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