theorem :: SURREALO:27

for X being set
for x, y, z, t being Surreal st x <= y & z = [X,{x,y}] & t = [X,{x}] holds
z == t