let x, y be Surreal; :: thesis: ( x is uSurreal & y is uSurreal & x == y implies x = y )
assume A1: ( x is uSurreal & y is uSurreal & x == y ) ; :: thesis: x = y
thus x = Unique_No x by A1, Def11
.= Unique_No y by A1, Th41
.= y by A1, Def11 ; :: thesis: verum