theorem Th8: :: SURREALC:8

for x, y being Surreal st x is positive & x == y holds
x,y are_commensurate by Th2, Th5;