theorem Th3: :: SURREALC:3

for x, y being Surreal st x,y are_commensurate holds
x is positive