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