let X be set ; :: thesis: for x, y, z, t being Surreal st x <= y & z = [X,{x,y}] & t = [X,{x}] holds
z == t
let x, y, z, t be Surreal; :: thesis: ( x <= y & z = [X,{x,y}] & t = [X,{x}] implies z == t )
assume A1: ( x <= y & z = [X,{x,y}] & t = [X,{x}] ) ; :: thesis: z == t
A2: for s being Surreal st s in R_ z holds
x <= s by A1, TARSKI:def 2;
A3: x in R_ z by A1, TARSKI:def 2;
t = [(L_ z),{x}] by A1;
hence z == t by A2, A3, Th24; :: thesis: verum