reconsider xx = x, yy = y as Surreal by A1;
take xx + yy ; :: thesis: for x1, y1 being Surreal st x1 = x & y1 = y holds
xx + yy = x1 + y1
thus for x1, y1 being Surreal st x1 = x & y1 = y holds
xx + yy = x1 + y1 ; :: thesis: verum