theorem :: SURREALN:60

for x, y being Surreal st x == y holds
real_qua x == real_qua y by Lm20;